Theorem mendplusg

Description: A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015)

	Ref	Expression
Hypotheses	mendplusgfval.a	$$⊢A=\mathrm{MEndo}\left(M\right)$$
	mendplusgfval.b	$$⊢B={\mathrm{Base}}_A$$
	mendplusgfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	mendplusg.q	$$⊢\underset{\dot{}}{✚}={+}_A$$
Assertion	mendplusg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$

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		mendplusg.q	$$⊢\underset{\dot{}}{✚}={+}_A$$
5		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to x{\underset{\dot{}}{+}}_{f}y=X{\underset{\dot{}}{+}}_{f}Y$$
6	1 2 3	mendplusgfval	$$⊢{+}_A=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$
7	4 6	eqtri	$$⊢\underset{\dot{}}{✚}=\left(x\in B,y\in B⟼x{\underset{\dot{}}{+}}_{f}y\right)$$
8		ovex	$$⊢X{\underset{\dot{}}{+}}_{f}Y\in \mathrm{V}$$
9	5 7 8	ovmpoa	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{✚}Y=X{\underset{\dot{}}{+}}_{f}Y$$