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	$$⊢\mathrm{EDRing}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cedring	$$class\mathrm{EDRing}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		cbs	$$class\mathrm{Base}$$
8		cnx	$$class\mathrm{ndx}$$
9	8 7	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
10		ctendo	$$class\mathrm{TEndo}$$
11	5 10	cfv	$$class\mathrm{TEndo}\left(k\right)$$
12	3	cv	$$setvarw$$
13	12 11	cfv	$$class\mathrm{TEndo}\left(k\right)\left(w\right)$$
14	9 13	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩$$
15		cplusg	$$class{+}_{𝑔}$$
16	8 15	cfv	$$class{+}_{\mathrm{ndx}}$$
17		vs	$$setvars$$
18		vt	$$setvart$$
19		vf	$$setvarf$$
20		cltrn	$$class\mathrm{LTrn}$$
21	5 20	cfv	$$class\mathrm{LTrn}\left(k\right)$$
22	12 21	cfv	$$class\mathrm{LTrn}\left(k\right)\left(w\right)$$
23	17	cv	$$setvars$$
24	19	cv	$$setvarf$$
25	24 23	cfv	$$classs\left(f\right)$$
26	18	cv	$$setvart$$
27	24 26	cfv	$$classt\left(f\right)$$
28	25 27	ccom	$$class\left(s\left(f\right)\circ t\left(f\right)\right)$$
29	19 22 28	cmpt	$$class\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)$$
30	17 18 13 13 29	cmpo	$$class\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
31	16 30	cop	$$class⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩$$
32		cmulr	$$class{\cdot }_{𝑟}$$
33	8 32	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
34	23 26	ccom	$$class\left(s\circ t\right)$$
35	17 18 13 13 34	cmpo	$$class\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)$$
36	33 35	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩$$
37	14 31 36	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩\right\}$$
38	3 6 37	cmpt	$$class\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩\right\}\right)$$
39	1 2 38	cmpt	$$class\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩\right\}\right)\right)$$
40	0 39	wceq	$$wff\mathrm{EDRing}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{TEndo}\left(k\right)\left(w\right)⟩,⟨{+}_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼\left(f\in \mathrm{LTrn}\left(k\right)\left(w\right)⟼s\left(f\right)\circ t\left(f\right)\right)\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(s\in \mathrm{TEndo}\left(k\right)\left(w\right),t\in \mathrm{TEndo}\left(k\right)\left(w\right)⟼s\circ t\right)⟩\right\}\right)\right)$$