Theorem mendplusgfval

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

	Ref	Expression
Hypotheses	mendplusgfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendplusgfval.b	$$⊢B={\mathrm{Base}}_A$$
	mendplusgfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	mendplusgfval	$$⊢{+}_A=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mendplusgfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
2		mendplusgfval.b	$$⊢B={\mathrm{Base}}_A$$
3		mendplusgfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
4	1	mendbas	$$⊢M\mathrm{LMHom}M={\mathrm{Base}}_A$$
5	2 4	eqtr4i	$$⊢B=M\mathrm{LMHom}M$$
6		ofeq	$$⊢\underset{\dot{}}{+}={+}_M\to {\circ }_f\underset{\dot{}}{+}={\circ }_f{+}_M$$
7	3 6	ax-mp	$$⊢{\circ }_f\underset{\dot{}}{+}={\circ }_f{+}_M$$
8	7	oveqi	$$⊢x{\underset{\dot{}}{+}}_{f}y=x{{+}_M}_{f}y$$
9	8	a1i	$$⊢\left(x\in B\wedge y\in B\right)\to x{\underset{\dot{}}{+}}_{f}y=x{{+}_M}_{f}y$$
10	9	mpoeq3ia	$$⊢\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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	$$⊢\mathrm{Scalar}\left(M\right)=\mathrm{Scalar}\left(M\right)$$
13		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)$$
14	5 10 11 12 13	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{\underset{\dot{}}{+}}_{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	1 14	syl5eq	$$⊢M\in \mathrm{V}\to A=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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\}$$
16	15	fveq2d	$$⊢M\in \mathrm{V}\to {+}_A={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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	2	fvexi	$$⊢B\in \mathrm{V}$$
18	17 17	mpoex	$$⊢\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)\in \mathrm{V}$$
19		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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{\underset{\dot{}}{+}}_{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\}$$
20	19	algaddg	$$⊢\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)\in \mathrm{V}\to \left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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)}$$
21	18 20	mp1i	$$⊢M\in \mathrm{V}\to \left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{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)}$$
22	16 21	eqtr4d	$$⊢M\in \mathrm{V}\to {+}_A=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$
23		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{MEndo}\left(M\right)=\varnothing$$
24	1 23	syl5eq	$$⊢\neg M\in \mathrm{V}\to A=\varnothing$$
25	24	fveq2d	$$⊢\neg M\in \mathrm{V}\to {+}_A={+}_{\varnothing }$$
26		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
27	26	str0	$$⊢\varnothing ={+}_{\varnothing }$$
28	25 27	eqtr4di	$$⊢\neg M\in \mathrm{V}\to {+}_A=\varnothing$$
29	24	fveq2d	$$⊢\neg M\in \mathrm{V}\to {\mathrm{Base}}_A={\mathrm{Base}}_{\varnothing }$$
30		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
31	29 2 30	3eqtr4g	$$⊢\neg M\in \mathrm{V}\to B=\varnothing$$
32	31	olcd	$$⊢\neg M\in \mathrm{V}\to \left(B=\varnothing \vee B=\varnothing \right)$$
33		0mpo0	$$⊢\left(B=\varnothing \vee B=\varnothing \right)\to \left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)=\varnothing$$
34	32 33	syl	$$⊢\neg M\in \mathrm{V}\to \left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)=\varnothing$$
35	28 34	eqtr4d	$$⊢\neg M\in \mathrm{V}\to {+}_A=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$
36	22 35	pm2.61i	$$⊢{+}_A=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$