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 39222
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 39220 . 2 class EDRingR
2 vk . . 3 setvar π‘˜
3 cvv 3446 . . 3 class V
4 vw . . . 4 setvar 𝑀
52cv 1541 . . . . 5 class π‘˜
6 clh 38450 . . . . 5 class LHyp
75, 6cfv 6497 . . . 4 class (LHypβ€˜π‘˜)
8 cnx 17066 . . . . . . 7 class ndx
9 cbs 17084 . . . . . . 7 class Base
108, 9cfv 6497 . . . . . 6 class (Baseβ€˜ndx)
114cv 1541 . . . . . . 7 class 𝑀
12 ctendo 39218 . . . . . . . 8 class TEndo
135, 12cfv 6497 . . . . . . 7 class (TEndoβ€˜π‘˜)
1411, 13cfv 6497 . . . . . 6 class ((TEndoβ€˜π‘˜)β€˜π‘€)
1510, 14cop 4593 . . . . 5 class ⟨(Baseβ€˜ndx), ((TEndoβ€˜π‘˜)β€˜π‘€)⟩
16 cplusg 17134 . . . . . . 7 class +g
178, 16cfv 6497 . . . . . 6 class (+gβ€˜ndx)
18 vs . . . . . . 7 setvar 𝑠
19 vt . . . . . . 7 setvar 𝑑
20 vf . . . . . . . 8 setvar 𝑓
21 cltrn 38567 . . . . . . . . . 10 class LTrn
225, 21cfv 6497 . . . . . . . . 9 class (LTrnβ€˜π‘˜)
2311, 22cfv 6497 . . . . . . . 8 class ((LTrnβ€˜π‘˜)β€˜π‘€)
2420cv 1541 . . . . . . . . . 10 class 𝑓
2518cv 1541 . . . . . . . . . 10 class 𝑠
2624, 25cfv 6497 . . . . . . . . 9 class (π‘ β€˜π‘“)
2719cv 1541 . . . . . . . . . 10 class 𝑑
2824, 27cfv 6497 . . . . . . . . 9 class (π‘‘β€˜π‘“)
2926, 28ccom 5638 . . . . . . . 8 class ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))
3020, 23, 29cmpt 5189 . . . . . . 7 class (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“)))
3118, 19, 14, 14, 30cmpo 7360 . . . . . 6 class (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))
3217, 31cop 4593 . . . . 5 class ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩
33 cmulr 17135 . . . . . . 7 class .r
348, 33cfv 6497 . . . . . 6 class (.rβ€˜ndx)
3527, 25ccom 5638 . . . . . . 7 class (𝑑 ∘ 𝑠)
3618, 19, 14, 14, 35cmpo 7360 . . . . . 6 class (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑑 ∘ 𝑠))
3734, 36cop 4593 . . . . 5 class ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑑 ∘ 𝑠))⟩
3815, 32, 37ctp 4591 . . . 4 class {⟨(Baseβ€˜ndx), ((TEndoβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑑 ∘ 𝑠))⟩}
394, 7, 38cmpt 5189 . . 3 class (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑑 ∘ 𝑠))⟩})
402, 3, 39cmpt 5189 . 2 class (π‘˜ ∈ V ↦ (𝑀 ∈ (LHypβ€˜π‘˜) ↦ {⟨(Baseβ€˜ndx), ((TEndoβ€˜π‘˜)β€˜π‘€)⟩, ⟨(+gβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑓 ∈ ((LTrnβ€˜π‘˜)β€˜π‘€) ↦ ((π‘ β€˜π‘“) ∘ (π‘‘β€˜π‘“))))⟩, ⟨(.rβ€˜ndx), (𝑠 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€), 𝑑 ∈ ((TEndoβ€˜π‘˜)β€˜π‘€) ↦ (𝑑 ∘ 𝑠))⟩}))
411, 40wceq 1542 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  39273
  Copyright terms: Public domain W3C validator