Theorem resvcmn

Description: Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018)

	Ref	Expression
Hypothesis	resvbas.1	|- H = ( G |`v A )
Assertion	resvcmn	|- ( A e. V -> ( G e. CMnd <-> H e. CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	|- H = ( G |`v A )
2		eqidd	|- ( A e. V -> ( Base ` G ) = ( Base ` G ) )
3		eqid	|- ( Base ` G ) = ( Base ` G )
4	1 3	resvbas	|- ( A e. V -> ( Base ` G ) = ( Base ` H ) )
5		eqid	|- ( +g ` G ) = ( +g ` G )
6	1 5	resvplusg	|- ( A e. V -> ( +g ` G ) = ( +g ` H ) )
7	6	oveqdr	|- ( ( A e. V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
8	2 4 7	cmnpropd	|- ( A e. V -> ( G e. CMnd <-> H e. CMnd ) )