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		ofeq	$$⊢{+}_m={+}_M\to {\circ }_f{+}_m={\circ }_f{+}_M$$
17	15 16	syl	$$⊢m=M\to {\circ }_f{+}_m={\circ }_f{+}_M$$
18	17	oveqdr	$$⊢\left(m=M\wedge b=B\right)\to x{{+}_m}_{f}y=x{{+}_M}_{f}y$$
19	13 13 18	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)$$
20	19 2	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x{{+}_m}_{f}y\right)=\underset{\dot{}}{+}$$
21	20	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{}}{+}⟩$$
22		eqidd	$$⊢\left(m=M\wedge b=B\right)\to x\circ y=x\circ y$$
23	13 13 22	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)$$
24	23 3	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \left(x\in b,y\in b⟼x\circ y\right)=\underset{\dot{}}{\times }$$
25	24	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 }⟩$$
26	14 21 25	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\}$$
27		fveq2	$$⊢m=M\to \mathrm{Scalar}\left(m\right)=\mathrm{Scalar}\left(M\right)$$
28	27	adantr	$$⊢\left(m=M\wedge b=B\right)\to \mathrm{Scalar}\left(m\right)=\mathrm{Scalar}\left(M\right)$$
29	28 4	eqtr4di	$$⊢\left(m=M\wedge b=B\right)\to \mathrm{Scalar}\left(m\right)=S$$
30	29	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⟩$$
31	29	fveq2d	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}={\mathrm{Base}}_S$$
32		fveq2	$$⊢m=M\to {\cdot }_m={\cdot }_M$$
33	32	adantr	$$⊢\left(m=M\wedge b=B\right)\to {\cdot }_m={\cdot }_M$$
34		ofeq	$$⊢{\cdot }_m={\cdot }_M\to {\circ }_f{\cdot }_m={\circ }_f{\cdot }_M$$
35	33 34	syl	$$⊢\left(m=M\wedge b=B\right)\to {\circ }_f{\cdot }_m={\circ }_f{\cdot }_M$$
36		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
37	36	adantr	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
38	37	xpeq1d	$$⊢\left(m=M\wedge b=B\right)\to {\mathrm{Base}}_m\times \left\{x\right\}={\mathrm{Base}}_M\times \left\{x\right\}$$
39		eqidd	$$⊢\left(m=M\wedge b=B\right)\to y=y$$
40	35 38 39	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$$
41	31 13 40	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)$$
42	41 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{}}{·}$$
43	42	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{}}{·}⟩$$
44	30 43	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\}$$
45	26 44	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\}$$
46	12 45	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\}$$
47	10 46	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\}$$
48		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)$$
49		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\in \mathrm{V}$$
50		prex	$$⊢\left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
51	49 50	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}$$
52	47 48 51	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\}$$
53	6 52	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\}$$