Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-edring-rN Structured version   Visualization version   GIF version

Definition df-edring-rN 36463
 Description: Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)
Assertion
Ref Expression
df-edring-rN EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}))
Distinct variable group:   𝑤,𝑘,𝑓,𝑠,𝑡

Detailed syntax breakdown of Definition df-edring-rN
StepHypRef Expression
1 cedring-rN 36461 . 2 class EDRingR
2 vk . . 3 setvar 𝑘
3 cvv 3304 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1595 . . . . 5 class 𝑘
6 clh 35690 . . . . 5 class LHyp
75, 6cfv 6001 . . . 4 class (LHyp‘𝑘)
8 cnx 15977 . . . . . . 7 class ndx
9 cbs 15980 . . . . . . 7 class Base
108, 9cfv 6001 . . . . . 6 class (Base‘ndx)
114cv 1595 . . . . . . 7 class 𝑤
12 ctendo 36459 . . . . . . . 8 class TEndo
135, 12cfv 6001 . . . . . . 7 class (TEndo‘𝑘)
1411, 13cfv 6001 . . . . . 6 class ((TEndo‘𝑘)‘𝑤)
1510, 14cop 4291 . . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16 cplusg 16064 . . . . . . 7 class +g
178, 16cfv 6001 . . . . . 6 class (+g‘ndx)
18 vs . . . . . . 7 setvar 𝑠
19 vt . . . . . . 7 setvar 𝑡
20 vf . . . . . . . 8 setvar 𝑓
21 cltrn 35807 . . . . . . . . . 10 class LTrn
225, 21cfv 6001 . . . . . . . . 9 class (LTrn‘𝑘)
2311, 22cfv 6001 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
2420cv 1595 . . . . . . . . . 10 class 𝑓
2518cv 1595 . . . . . . . . . 10 class 𝑠
2624, 25cfv 6001 . . . . . . . . 9 class (𝑠𝑓)
2719cv 1595 . . . . . . . . . 10 class 𝑡
2824, 27cfv 6001 . . . . . . . . 9 class (𝑡𝑓)
2926, 28ccom 5222 . . . . . . . 8 class ((𝑠𝑓) ∘ (𝑡𝑓))
3020, 23, 29cmpt 4837 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓)))
3118, 19, 14, 14, 30cmpt2 6767 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
3217, 31cop 4291 . . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩
33 cmulr 16065 . . . . . . 7 class .r
348, 33cfv 6001 . . . . . 6 class (.r‘ndx)
3527, 25ccom 5222 . . . . . . 7 class (𝑡𝑠)
3618, 19, 14, 14, 35cmpt2 6767 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))
3734, 36cop 4291 . . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩
3815, 32, 37ctp 4289 . . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}
394, 7, 38cmpt 4837 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩})
402, 3, 39cmpt 4837 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}))
411, 40wceq 1596 1 wff EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}))
 Colors of variables: wff setvar class This definition is referenced by:  erngfset-rN  36514
 Copyright terms: Public domain W3C validator