Theorem mendmulrfval

Description: Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	mendmulrfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendmulrfval.b	$$⊢B={\mathrm{Base}}_A$$
Assertion	mendmulrfval	$$⊢{\cdot }_A=\left(x\in B,y\in B⟼x\circ y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mendmulrfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
2		mendmulrfval.b	$$⊢B={\mathrm{Base}}_A$$
3	1	mendbas	$$⊢M\mathrm{LMHom}M={\mathrm{Base}}_A$$
4	2 3	eqtr4i	$$⊢B=M\mathrm{LMHom}M$$
5		eqid	$$⊢\left(x\in B,y\in B⟼x{{+}_M}_{f}y\right)=\left(x\in B,y\in B⟼x{{+}_M}_{f}y\right)$$
6		eqid	$$⊢\left(x\in B,y\in B⟼x\circ y\right)=\left(x\in B,y\in B⟼x\circ y\right)$$
7		eqid	$$⊢\mathrm{Scalar}\left(M\right)=\mathrm{Scalar}\left(M\right)$$
8		eqid	$$⊢\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}}_{\mathrm{Scalar}\left(M\right)},y\in B⟼\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y\right)$$
9	4 5 6 7 8	mendval	$$⊢M\in \mathrm{V}\to \mathrm{MEndo}\left(M\right)=\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\}$$
10	1 9	syl5eq	$$⊢M\in \mathrm{V}\to A=\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\}$$
11	10	fveq2d	$$⊢M\in \mathrm{V}\to {\cdot }_A={\cdot }_{\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)}$$
12	2	fvexi	$$⊢B\in \mathrm{V}$$
13	12 12	mpoex	$$⊢\left(x\in B,y\in B⟼x\circ y\right)\in \mathrm{V}$$
14		eqid	$$⊢\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}},\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\}$$
15	14	algmulr	$$⊢\left(x\in B,y\in B⟼x\circ y\right)\in \mathrm{V}\to \left(x\in B,y\in B⟼x\circ y\right)={\cdot }_{\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)}$$
16	13 15	mp1i	$$⊢M\in \mathrm{V}\to \left(x\in B,y\in B⟼x\circ y\right)={\cdot }_{\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)}$$
17	11 16	eqtr4d	$$⊢M\in \mathrm{V}\to {\cdot }_A=\left(x\in B,y\in B⟼x\circ y\right)$$
18		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{MEndo}\left(M\right)=\varnothing$$
19	1 18	syl5eq	$$⊢\neg M\in \mathrm{V}\to A=\varnothing$$
20	19	fveq2d	$$⊢\neg M\in \mathrm{V}\to {\cdot }_A={\cdot }_{\varnothing }$$
21		mulrid	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
22	21	str0	$$⊢\varnothing ={\cdot }_{\varnothing }$$
23	20 22	eqtr4di	$$⊢\neg M\in \mathrm{V}\to {\cdot }_A=\varnothing$$
24	19	fveq2d	$$⊢\neg M\in \mathrm{V}\to {\mathrm{Base}}_A={\mathrm{Base}}_{\varnothing }$$
25	2 24	syl5eq	$$⊢\neg M\in \mathrm{V}\to B={\mathrm{Base}}_{\varnothing }$$
26		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
27	25 26	eqtr4di	$$⊢\neg M\in \mathrm{V}\to B=\varnothing$$
28	27	olcd	$$⊢\neg M\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
29		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(x\in B,y\in B⟼x\circ y\right)=\varnothing$$
30	28 29	syl	$$⊢\neg M\in \mathrm{V}\to \left(x\in B,y\in B⟼x\circ y\right)=\varnothing$$
31	23 30	eqtr4d	$$⊢\neg M\in \mathrm{V}\to {\cdot }_A=\left(x\in B,y\in B⟼x\circ y\right)$$
32	17 31	pm2.61i	$$⊢{\cdot }_A=\left(x\in B,y\in B⟼x\circ y\right)$$