Users' Mathboxes 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 38508
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 38504 . 2 class EDRing
2 vk . . 3 setvar 𝑘
3 cvv 3408 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1542 . . . . 5 class 𝑘
6 clh 37735 . . . . 5 class LHyp
75, 6cfv 6380 . . . 4 class (LHyp‘𝑘)
8 cnx 16744 . . . . . . 7 class ndx
9 cbs 16760 . . . . . . 7 class Base
108, 9cfv 6380 . . . . . 6 class (Base‘ndx)
114cv 1542 . . . . . . 7 class 𝑤
12 ctendo 38503 . . . . . . . 8 class TEndo
135, 12cfv 6380 . . . . . . 7 class (TEndo‘𝑘)
1411, 13cfv 6380 . . . . . 6 class ((TEndo‘𝑘)‘𝑤)
1510, 14cop 4547 . . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16 cplusg 16802 . . . . . . 7 class +g
178, 16cfv 6380 . . . . . 6 class (+g‘ndx)
18 vs . . . . . . 7 setvar 𝑠
19 vt . . . . . . 7 setvar 𝑡
20 vf . . . . . . . 8 setvar 𝑓
21 cltrn 37852 . . . . . . . . . 10 class LTrn
225, 21cfv 6380 . . . . . . . . 9 class (LTrn‘𝑘)
2311, 22cfv 6380 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
2420cv 1542 . . . . . . . . . 10 class 𝑓
2518cv 1542 . . . . . . . . . 10 class 𝑠
2624, 25cfv 6380 . . . . . . . . 9 class (𝑠𝑓)
2719cv 1542 . . . . . . . . . 10 class 𝑡
2824, 27cfv 6380 . . . . . . . . 9 class (𝑡𝑓)
2926, 28ccom 5555 . . . . . . . 8 class ((𝑠𝑓) ∘ (𝑡𝑓))
3020, 23, 29cmpt 5135 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓)))
3118, 19, 14, 14, 30cmpo 7215 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
3217, 31cop 4547 . . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩
33 cmulr 16803 . . . . . . 7 class .r
348, 33cfv 6380 . . . . . 6 class (.r‘ndx)
3525, 27ccom 5555 . . . . . . 7 class (𝑠𝑡)
3618, 19, 14, 14, 35cmpo 7215 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))
3734, 36cop 4547 . . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩
3815, 32, 37ctp 4545 . . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩}
394, 7, 38cmpt 5135 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩})
402, 3, 39cmpt 5135 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠𝑡))⟩}))
411, 40wceq 1543 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  38550
  Copyright terms: Public domain W3C validator