Theorem mendmulr

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

	Ref	Expression
Hypotheses	mendmulrfval.a	|- A = ( MEndo ` M )
	mendmulrfval.b	|- B = ( Base ` A )
	mendmulr.q	|- .x. = ( .r ` A )
Assertion	mendmulr	|- ( ( X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X o. Y ) )

Proof

Step	Hyp	Ref	Expression
1		mendmulrfval.a	|- A = ( MEndo ` M )
2		mendmulrfval.b	|- B = ( Base ` A )
3		mendmulr.q	|- .x. = ( .r ` A )
4		coexg	|- ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
5		coeq1	|- ( x = X -> ( x o. y ) = ( X o. y ) )
6		coeq2	|- ( y = Y -> ( X o. y ) = ( X o. Y ) )
7	1 2	mendmulrfval	|- ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) )
8	3 7	eqtri	|- .x. = ( x e. B , y e. B |-> ( x o. y ) )
9	5 6 8	ovmpog	|- ( ( X e. B /\ Y e. B /\ ( X o. Y ) e. _V ) -> ( X .x. Y ) = ( X o. Y ) )
10	4 9	mpd3an3	|- ( ( X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X o. Y ) )