Metamath Proof Explorer

Definition df-edring-rN

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)

Ref Expression
Assertion df-edring-rN EDRingR = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring-rN ⊢ EDRingR
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 cbs ⊢ Base
8 cnx ⊢ ndx
9 8 7 cfv ⊢ ( Base ‘ ndx )
10 ctendo ⊢ TEndo
11 5 10 cfv ⊢ ( TEndo ‘ 𝑘 )
12 3 cv ⊢ 𝑤
13 12 11 cfv ⊢ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 )
14 9 13 cop ⊢ ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩
15 cplusg ⊢ +g
16 8 15 cfv ⊢ ( +g ‘ ndx )
17 vs ⊢ 𝑠
18 vt ⊢ 𝑡
19 vf ⊢ 𝑓
20 cltrn ⊢ LTrn
21 5 20 cfv ⊢ ( LTrn ‘ 𝑘 )
22 12 21 cfv ⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
23 17 cv ⊢ 𝑠
24 19 cv ⊢ 𝑓
25 24 23 cfv ⊢ ( 𝑠 ‘ 𝑓 )
26 18 cv ⊢ 𝑡
27 24 26 cfv ⊢ ( 𝑡 ‘ 𝑓 )
28 25 27 ccom ⊢ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) )
29 19 22 28 cmpt ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) )
30 17 18 13 13 29 cmpo ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
31 16 30 cop ⊢ ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩
32 cmulr ⊢ .r
33 8 32 cfv ⊢ ( .r ‘ ndx )
34 26 23 ccom ⊢ ( 𝑡 ∘ 𝑠 )
35 17 18 13 13 34 cmpo ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) )
36 33 35 cop ⊢ ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩
37 14 31 36 ctp ⊢ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ }
38 3 6 37 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } )
39 1 2 38 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } ) )
40 0 39 wceq ⊢ EDRingR = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑡 ∘ 𝑠 ) ) ⟩ } ) )