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

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

Detailed syntax breakdown of Definition df-edring
StepHypRef Expression
1 cedring 35059 . 2 class EDRing
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1474 . . . . 5 class 𝑘
6 clh 34288 . . . . 5 class LHyp
75, 6cfv 5804 . . . 4 class (LHyp‘𝑘)
8 cnx 15692 . . . . . . 7 class ndx
9 cbs 15695 . . . . . . 7 class Base
108, 9cfv 5804 . . . . . 6 class (Base‘ndx)
114cv 1474 . . . . . . 7 class 𝑤
12 ctendo 35058 . . . . . . . 8 class TEndo
135, 12cfv 5804 . . . . . . 7 class (TEndo‘𝑘)
1411, 13cfv 5804 . . . . . 6 class ((TEndo‘𝑘)‘𝑤)
1510, 14cop 4131 . . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16 cplusg 15768 . . . . . . 7 class +g
178, 16cfv 5804 . . . . . 6 class (+g‘ndx)
18 vs . . . . . . 7 setvar 𝑠
19 vt . . . . . . 7 setvar 𝑡
20 vf . . . . . . . 8 setvar 𝑓
21 cltrn 34405 . . . . . . . . . 10 class LTrn
225, 21cfv 5804 . . . . . . . . 9 class (LTrn‘𝑘)
2311, 22cfv 5804 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
2420cv 1474 . . . . . . . . . 10 class 𝑓
2518cv 1474 . . . . . . . . . 10 class 𝑠
2624, 25cfv 5804 . . . . . . . . 9 class (𝑠𝑓)
2719cv 1474 . . . . . . . . . 10 class 𝑡
2824, 27cfv 5804 . . . . . . . . 9 class (𝑡𝑓)
2926, 28ccom 5042 . . . . . . . 8 class ((𝑠𝑓) ∘ (𝑡𝑓))
3020, 23, 29cmpt 4643 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓)))
3118, 19, 14, 14, 30cmpt2 6551 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
3217, 31cop 4131 . . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩
33 cmulr 15769 . . . . . . 7 class .r
348, 33cfv 5804 . . . . . 6 class (.r‘ndx)
3525, 27ccom 5042 . . . . . . 7 class (𝑠𝑡)
3618, 19, 14, 14, 35cmpt2 6551 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))
3734, 36cop 4131 . . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩
3815, 32, 37ctp 4129 . . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩}
394, 7, 38cmpt 4643 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩})
402, 3, 39cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩}))
411, 40wceq 1475 1 wff EDRing = (𝑘 ∈ 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  35105
 Copyright terms: Public domain W3C validator