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 ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ∘ 𝑡 ) ) ⟩ } ) )