Definition df-mend

Description: Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015)

	Ref	Expression
Assertion	df-mend	$$⊢\mathrm{MEndo}=\left(m\in \mathrm{V}⟼⦋\left(m\mathrm{LMHom}m\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmend	$$class\mathrm{MEndo}$$
1		vm	$$setvarm$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarm$$
4		clmhm	$$class\mathrm{LMHom}$$
5	3 3 4	co	$$class\left(m\mathrm{LMHom}m\right)$$
6		vb	$$setvarb$$
7		cbs	$$class\mathrm{Base}$$
8		cnx	$$class\mathrm{ndx}$$
9	8 7	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
10	6	cv	$$setvarb$$
11	9 10	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
12		cplusg	$$class{+}_{𝑔}$$
13	8 12	cfv	$$class{+}_{\mathrm{ndx}}$$
14		vx	$$setvarx$$
15		vy	$$setvary$$
16	14	cv	$$setvarx$$
17	3 12	cfv	$$class{+}_m$$
18	17	cof	$$class{\circ }_f{+}_m$$
19	15	cv	$$setvary$$
20	16 19 18	co	$$class\left(x{{+}_m}_{f}y\right)$$
21	14 15 10 10 20	cmpo	$$class\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)$$
22	13 21	cop	$$class⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩$$
23		cmulr	$$class{\cdot }_{𝑟}$$
24	8 23	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
25	16 19	ccom	$$class\left(x\circ y\right)$$
26	14 15 10 10 25	cmpo	$$class\left(x\in b,y\in b⟼x\circ y\right)$$
27	24 26	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩$$
28	11 22 27	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}$$
29		csca	$$class\mathrm{Scalar}$$
30	8 29	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
31	3 29	cfv	$$class\mathrm{Scalar}\left(m\right)$$
32	30 31	cop	$$class⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩$$
33		cvsca	$$class{\cdot }_{𝑠}$$
34	8 33	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
35	31 7	cfv	$$class{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}$$
36	3 7	cfv	$$class{\mathrm{Base}}_m$$
37	16	csn	$$class\left\{x\right\}$$
38	36 37	cxp	$$class\left({\mathrm{Base}}_m\times \left\{x\right\}\right)$$
39	3 33	cfv	$$class{\cdot }_m$$
40	39	cof	$$class{\circ }_f{\cdot }_m$$
41	38 19 40	co	$$class\left(\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)$$
42	14 15 35 10 41	cmpo	$$class\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)$$
43	34 42	cop	$$class⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩$$
44	32 43	cpr	$$class\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}$$
45	28 44	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}\right)$$
46	6 5 45	csb	$$class⦋\left(m\mathrm{LMHom}m\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}\right)$$
47	1 2 46	cmpt	$$class\left(m\in \mathrm{V}⟼⦋\left(m\mathrm{LMHom}m\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}\right)\right)$$
48	0 47	wceq	$$wff\mathrm{MEndo}=\left(m\in \mathrm{V}⟼⦋\left(m\mathrm{LMHom}m\right)/b⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)},y\in b⟼\left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y\right)⟩\right\}\right)\right)$$