Theorem resvcmn

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

	Ref	Expression
Hypothesis	resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
Assertion	resvcmn	$$⊢A\in V\to \left(G\in \mathrm{CMnd}\leftrightarrow H\in \mathrm{CMnd}\right)$$

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
2		eqidd	$$⊢A\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	1 3	resvbas	$$⊢A\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_H$$
5		eqid	$$⊢{+}_G={+}_G$$
6	1 5	resvplusg	$$⊢A\in V\to {+}_G={+}_H$$
7	6	oveqdr	$$⊢\left(A\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{H}y$$
8	2 4 7	cmnpropd	$$⊢A\in V\to \left(G\in \mathrm{CMnd}\leftrightarrow H\in \mathrm{CMnd}\right)$$