Theorem mendvscafval

Description: Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 3-Mar-2024)

	Ref	Expression
Hypotheses	mendvscafval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendvscafval.v	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
	mendvscafval.b	$$⊢B={\mathrm{Base}}_A$$
	mendvscafval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
	mendvscafval.k	$$⊢K={\mathrm{Base}}_S$$
	mendvscafval.e	$$⊢E={\mathrm{Base}}_M$$
Assertion	mendvscafval	$$⊢{\cdot }_A=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
2		mendvscafval.v	$$⊢\underset{\dot{}}{·}={\cdot }_M$$
3		mendvscafval.b	$$⊢B={\mathrm{Base}}_A$$
4		mendvscafval.s	$$⊢S=\mathrm{Scalar}\left(M\right)$$
5		mendvscafval.k	$$⊢K={\mathrm{Base}}_S$$
6		mendvscafval.e	$$⊢E={\mathrm{Base}}_M$$
7	1	fveq2i	$$⊢{\cdot }_A={\cdot }_{\mathrm{MEndo}\left(M\right)}$$
8	1	mendbas	$$⊢M\mathrm{LMHom}M={\mathrm{Base}}_A$$
9	3 8	eqtr4i	$$⊢B=M\mathrm{LMHom}M$$
10		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)$$
11		eqid	$$⊢\left(x\in B,y\in B⟼x\circ y\right)=\left(x\in B,y\in B⟼x\circ y\right)$$
12		eqid	$$⊢B=B$$
13	6	xpeq1i	$$⊢E\times \left\{x\right\}={\mathrm{Base}}_M\times \left\{x\right\}$$
14		eqid	$$⊢y=y$$
15		ofeq	$$⊢\underset{\dot{}}{·}={\cdot }_M\to {\circ }_f\underset{\dot{}}{·}={\circ }_f{\cdot }_M$$
16	2 15	ax-mp	$$⊢{\circ }_f\underset{\dot{}}{·}={\circ }_f{\cdot }_M$$
17	13 14 16	oveq123i	$$⊢\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y=\left({\mathrm{Base}}_M\times \left\{x\right\}\right){{\cdot }_M}_{f}y$$
18	5 12 17	mpoeq123i	$$⊢\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{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)$$
19	9 10 11 4 18	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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)⟩\right\}$$
20	19	fveq2d	$$⊢M\in \mathrm{V}\to {\cdot }_{\mathrm{MEndo}\left(M\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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)⟩\right\}\right)}$$
21	5	fvexi	$$⊢K\in \mathrm{V}$$
22	3	fvexi	$$⊢B\in \mathrm{V}$$
23	21 22	mpoex	$$⊢\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)\in \mathrm{V}$$
24		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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)⟩\right\}$$
25	24	algvsca	$$⊢\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)\in \mathrm{V}\to \left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)⟩\right\}\right)}$$
26	23 25	mp1i	$$⊢M\in \mathrm{V}\to \left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}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),S⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)⟩\right\}\right)}$$
27	20 26	eqtr4d	$$⊢M\in \mathrm{V}\to {\cdot }_{\mathrm{MEndo}\left(M\right)}=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$
28		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{MEndo}\left(M\right)=\varnothing$$
29	28	fveq2d	$$⊢\neg M\in \mathrm{V}\to {\cdot }_{\mathrm{MEndo}\left(M\right)}={\cdot }_{\varnothing }$$
30		df-vsca	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}6$$
31	30	str0	$$⊢\varnothing ={\cdot }_{\varnothing }$$
32	29 31	eqtr4di	$$⊢\neg M\in \mathrm{V}\to {\cdot }_{\mathrm{MEndo}\left(M\right)}=\varnothing$$
33		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{Scalar}\left(M\right)=\varnothing$$
34	4 33	syl5eq	$$⊢\neg M\in \mathrm{V}\to S=\varnothing$$
35	34	fveq2d	$$⊢\neg M\in \mathrm{V}\to {\mathrm{Base}}_S={\mathrm{Base}}_{\varnothing }$$
36		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
37	35 5 36	3eqtr4g	$$⊢\neg M\in \mathrm{V}\to K=\varnothing$$
38	37	orcd	$$⊢\neg M\in \mathrm{V}\to \left(K=\varnothing \vee B=\varnothing \right)$$
39		0mpo0	$$⊢\left(K=\varnothing \vee B=\varnothing \right)\to \left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)=\varnothing$$
40	38 39	syl	$$⊢\neg M\in \mathrm{V}\to \left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)=\varnothing$$
41	32 40	eqtr4d	$$⊢\neg M\in \mathrm{V}\to {\cdot }_{\mathrm{MEndo}\left(M\right)}=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$
42	27 41	pm2.61i	$$⊢{\cdot }_{\mathrm{MEndo}\left(M\right)}=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$
43	7 42	eqtri	$$⊢{\cdot }_A=\left(x\in K,y\in B⟼\left(E\times \left\{x\right\}\right){\underset{\dot{}}{·}}_{f}y\right)$$