Theorem mendval

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

	Ref	Expression
Hypotheses	mendval.b	$$⊢B=M\mathrm{LMHom}M$$
	mendval.p	$$⊢\underset{\dot{}}{+}=\left(x\in B,y\in B⟼x{{+}_M}_{f}y\right)$$
	mendval.t	$$⊢\underset{\dot{}}{\times }=\left(x\in B,y\in B⟼x\circ y\right)$$
	mendval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	mendval.v	$$⊢\underset{\dot{}}{·}=\left(x\in {\mathrm{Base}}_S,y\in B⟼\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y\right)$$
Assertion	mendval	$$⊢M\in X\to \mathrm{MEndo}\left(M\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mendval.b	$$⊢B=M\mathrm{LMHom}M$$
2		mendval.p	$$⊢\underset{\dot{}}{+}=\left(x\in B,y\in B⟼x{{+}_M}_{f}y\right)$$
3		mendval.t	$$⊢\underset{\dot{}}{\times }=\left(x\in B,y\in B⟼x\circ y\right)$$
4		mendval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
5		mendval.v	$$⊢\underset{\dot{}}{·}=\left(x\in {\mathrm{Base}}_S,y\in B⟼\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y\right)$$
6		elex	$$⊢M\in X\to M\in \mathrm{V}$$
7		oveq12	$$⊢\left(m=M\wedge m=M\right)\to m\mathrm{LMHom}m=M\mathrm{LMHom}M$$
8	7	anidms	$$⊢m=M\to m\mathrm{LMHom}m=M\mathrm{LMHom}M$$
9	8 1	eqtr4di	$$⊢m=M\to m\mathrm{LMHom}m=B$$
10	9	csbeq1d	$$⊢m=M\to ⦋\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)=⦋B/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)$$
11		ovex	$$⊢m\mathrm{LMHom}m\in \mathrm{V}$$
12	9 11	eqeltrrdi	$$⊢m=M\to B\in \mathrm{V}$$
13		simpr	$$⊢\left(m=M\wedge b=B\right)\to b=B$$
14	13	opeq2d	$$⊢\left(m=M\wedge b=B\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩$$
15		fveq2	$$⊢m=M\to {+}_m={+}_M$$
16	15	ofeqd	$$⊢m=M\to {\circ }_f{+}_m={\circ }_f{+}_M$$
17	16	oveqdr	$$⊢\left(m=M\wedge b=B\right)\to x{{+}_m}_{f}y=x{{+}_M}_{f}y$$
18	13 13 17	mpoeq123dv	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)=\left(x\in B,y\in B⟼x{{+}_M}_{f}y\right)$$
19	18 2	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)=\underset{\dot{}}{+}$$
20	19	opeq2d	$$⊢\left(m=M\wedge b=B\right)\to ⟨{+}_{\mathrm{ndx}},\left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)⟩=⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩$$
21		eqidd	$$⊢\left(m=M\wedge b=B\right)\to x\circ y=x\circ y$$
22	13 13 21	mpoeq123dv	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x\circ y\right)=\left(x\in B,y\in B⟼x\circ y\right)$$
23	22 3	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x\circ y\right)=\underset{\dot{}}{\times }$$
24	23	opeq2d	$$⊢\left(m=M\wedge b=B\right)\to ⟨{\cdot }_{\mathrm{ndx}},\left(x\in b,y\in b⟼x\circ y\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩$$
25	14 20 24	tpeq123d	$$⊢\left(m=M\wedge b=B\right)\to \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\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}$$
26		fveq2	$$⊢m=M\to \mathrm{Scalar}\left(m\right)=\mathrm{Scalar}\left(M\right)$$
27	26	adantr	$$⊢\left(m=M\wedge b=B\right)\to \mathrm{Scalar}\left(m\right)=\mathrm{Scalar}\left(M\right)$$
28	27 4	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \mathrm{Scalar}\left(m\right)=S$$
29	28	opeq2d	$$⊢\left(m=M\wedge b=B\right)\to ⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(m\right)⟩=⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩$$
30	28	fveq2d	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}={\mathrm{Base}}_S$$
31		fveq2	$$⊢m=M\to {\cdot }_m={\cdot }_M$$
32	31	adantr	$$⊢\left(m=M\wedge b=B\right)\to {\cdot }_m={\cdot }_M$$
33	32	ofeqd	$$⊢\left(m=M\wedge b=B\right)\to {\circ }_f{\cdot }_m={\circ }_f{\cdot }_M$$
34		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
35	34	adantr	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
36	35	xpeq1d	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_m\times \left\{x\right\}={\mathrm{Base}}_M\times \left\{x\right\}$$
37		eqidd	$$⊢\left(m=M\wedge b=B\right)\to y=y$$
38	33 36 37	oveq123d	$$⊢\left(m=M\wedge b=B\right)\to \left({\mathrm{Base}}_m\times \left\{x\right\}\right){{\cdot }_m}_{f}y=\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y$$
39	30 13 38	mpoeq123dv	$$⊢\left(m=M\wedge b=B\right)\to \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)=\left(x\in {\mathrm{Base}}_S,y\in B⟼\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y\right)$$
40	39 5	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \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)=\underset{\dot{}}{·}$$
41	40	opeq2d	$$⊢\left(m=M\wedge b=B\right)\to ⟨{\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)⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
42	29 41	preq12d	$$⊢\left(m=M\wedge b=B\right)\to \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\}=\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
43	25 42	uneq12d	$$⊢\left(m=M\wedge b=B\right)\to \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\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
44	12 43	csbied	$$⊢m=M\to ⦋B/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)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
45	10 44	eqtrd	$$⊢m=M\to ⦋\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)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
46		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)$$
47		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\in \mathrm{V}$$
48		prex	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
49	47 48	unex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
50	45 46 49	fvmpt	$$⊢M\in \mathrm{V}\to \mathrm{MEndo}\left(M\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
51	6 50	syl	$$⊢M\in X\to \mathrm{MEndo}\left(M\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$