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 Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w s t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedring class EDRing
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp k
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 ctendo class TEndo
11 5 10 cfv class TEndo k
12 3 cv setvar w
13 12 11 cfv class TEndo k w
14 9 13 cop class Base ndx TEndo k w
15 cplusg class + 𝑔
16 8 15 cfv class + ndx
17 vs setvar s
18 vt setvar t
19 vf setvar f
20 cltrn class LTrn
21 5 20 cfv class LTrn k
22 12 21 cfv class LTrn k w
23 17 cv setvar s
24 19 cv setvar f
25 24 23 cfv class s f
26 18 cv setvar t
27 24 26 cfv class t f
28 25 27 ccom class s f t f
29 19 22 28 cmpt class f LTrn k w s f t f
30 17 18 13 13 29 cmpo class s TEndo k w , t TEndo k w f LTrn k w s f t f
31 16 30 cop class + ndx s 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 class s t
35 17 18 13 13 34 cmpo class s TEndo k w , t TEndo k w s t
36 33 35 cop class ndx s TEndo k w , t TEndo k w s t
37 14 31 36 ctp class Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w s t
38 3 6 37 cmpt class w LHyp k Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w s t
39 1 2 38 cmpt class k V w LHyp k Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w s t
40 0 39 wceq wff EDRing = k V w LHyp k Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w s t