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 = ( MEndo ` M )
	mendplusgfval.b	|- B = ( Base ` A )
	mendplusgfval.p	|- .+ = ( +g ` M )
	mendplusg.q	|- .+b = ( +g ` A )
Assertion	mendplusg	|- ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )

Proof

Step	Hyp	Ref	Expression
1		mendplusgfval.a	|- A = ( MEndo ` M )
2		mendplusgfval.b	|- B = ( Base ` A )
3		mendplusgfval.p	|- .+ = ( +g ` M )
4		mendplusg.q	|- .+b = ( +g ` A )
5		oveq12	|- ( ( x = X /\ y = Y ) -> ( x oF .+ y ) = ( X oF .+ Y ) )
6	1 2 3	mendplusgfval	|- ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) )
7	4 6	eqtri	|- .+b = ( x e. B , y e. B |-> ( x oF .+ y ) )
8		ovex	|- ( X oF .+ Y ) e. _V
9	5 7 8	ovmpoa	|- ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )