Metamath Proof Explorer


Definition df-edring

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)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring EDRing
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 23 26 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 EDRing = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { ⟨ ( Base ‘ ndx ) , ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( 𝑠𝑓 ) ∘ ( 𝑡𝑓 ) ) ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑡 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠𝑡 ) ) ⟩ } ) )