Users' Mathboxes 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 37772
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 37770 . 2 class EDRingR
2 vk . . 3 setvar 𝑘
3 cvv 3492 . . 3 class V
4 vw . . . 4 setvar 𝑤
52cv 1527 . . . . 5 class 𝑘
6 clh 37000 . . . . 5 class LHyp
75, 6cfv 6348 . . . 4 class (LHyp‘𝑘)
8 cnx 16468 . . . . . . 7 class ndx
9 cbs 16471 . . . . . . 7 class Base
108, 9cfv 6348 . . . . . 6 class (Base‘ndx)
114cv 1527 . . . . . . 7 class 𝑤
12 ctendo 37768 . . . . . . . 8 class TEndo
135, 12cfv 6348 . . . . . . 7 class (TEndo‘𝑘)
1411, 13cfv 6348 . . . . . 6 class ((TEndo‘𝑘)‘𝑤)
1510, 14cop 4563 . . . . 5 class ⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩
16 cplusg 16553 . . . . . . 7 class +g
178, 16cfv 6348 . . . . . 6 class (+g‘ndx)
18 vs . . . . . . 7 setvar 𝑠
19 vt . . . . . . 7 setvar 𝑡
20 vf . . . . . . . 8 setvar 𝑓
21 cltrn 37117 . . . . . . . . . 10 class LTrn
225, 21cfv 6348 . . . . . . . . 9 class (LTrn‘𝑘)
2311, 22cfv 6348 . . . . . . . 8 class ((LTrn‘𝑘)‘𝑤)
2420cv 1527 . . . . . . . . . 10 class 𝑓
2518cv 1527 . . . . . . . . . 10 class 𝑠
2624, 25cfv 6348 . . . . . . . . 9 class (𝑠𝑓)
2719cv 1527 . . . . . . . . . 10 class 𝑡
2824, 27cfv 6348 . . . . . . . . 9 class (𝑡𝑓)
2926, 28ccom 5552 . . . . . . . 8 class ((𝑠𝑓) ∘ (𝑡𝑓))
3020, 23, 29cmpt 5137 . . . . . . 7 class (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓)))
3118, 19, 14, 14, 30cmpo 7147 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))
3217, 31cop 4563 . . . . 5 class ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩
33 cmulr 16554 . . . . . . 7 class .r
348, 33cfv 6348 . . . . . 6 class (.r‘ndx)
3527, 25ccom 5552 . . . . . . 7 class (𝑡𝑠)
3618, 19, 14, 14, 35cmpo 7147 . . . . . 6 class (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))
3734, 36cop 4563 . . . . 5 class ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩
3815, 32, 37ctp 4561 . . . 4 class {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}
394, 7, 38cmpt 5137 . . 3 class (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩})
402, 3, 39cmpt 5137 . 2 class (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {⟨(Base‘ndx), ((TEndo‘𝑘)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠𝑓) ∘ (𝑡𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡𝑠))⟩}))
411, 40wceq 1528 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  37823
  Copyright terms: Public domain W3C validator