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=k∈V⟼w∈LHyp⁡k⟼BasendxTEndo⁡k⁡w+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring classEDRing
1 vk setvark
2 cvv classV
3 vw setvarw
4 clh classLHyp
5 1 cv setvark
6 5 4 cfv classLHyp⁡k
7 cbs classBase
8 cnx classndx
9 8 7 cfv classBasendx
10 ctendo classTEndo
11 5 10 cfv classTEndo⁡k
12 3 cv setvarw
13 12 11 cfv classTEndo⁡k⁡w
14 9 13 cop classBasendxTEndo⁡k⁡w
15 cplusg class+𝑔
16 8 15 cfv class+ndx
17 vs setvars
18 vt setvart
19 vf setvarf
20 cltrn classLTrn
21 5 20 cfv classLTrn⁡k
22 12 21 cfv classLTrn⁡k⁡w
23 17 cv setvars
24 19 cv setvarf
25 24 23 cfv classs⁡f
26 18 cv setvart
27 24 26 cfv classt⁡f
28 25 27 ccom classs⁡f∘t⁡f
29 19 22 28 cmpt classf∈LTrn⁡k⁡w⟼s⁡f∘t⁡f
30 17 18 13 13 29 cmpo classs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f
31 16 30 cop class+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f
32 cmulr class⋅𝑟
33 8 32 cfv class⋅ndx
34 23 26 ccom classs∘t
35 17 18 13 13 34 cmpo classs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t
36 33 35 cop class⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t
37 14 31 36 ctp classBasendxTEndo⁡k⁡w+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t
38 3 6 37 cmpt classw∈LHyp⁡k⟼BasendxTEndo⁡k⁡w+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t
39 1 2 38 cmpt classk∈V⟼w∈LHyp⁡k⟼BasendxTEndo⁡k⁡w+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t
40 0 39 wceq wffEDRing=k∈V⟼w∈LHyp⁡k⟼BasendxTEndo⁡k⁡w+ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼f∈LTrn⁡k⁡w⟼s⁡f∘t⁡f⋅ndxs∈TEndo⁡k⁡w,t∈TEndo⁡k⁡w⟼s∘t