Metamath Proof Explorer


Theorem resvcmn

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

Ref Expression
Hypothesis resvbas.1 𝐻 = ( 𝐺v 𝐴 )
Assertion resvcmn ( 𝐴𝑉 → ( 𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 𝐻 = ( 𝐺v 𝐴 )
2 eqidd ( 𝐴𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 1 3 resvbas ( 𝐴𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5 eqid ( +g𝐺 ) = ( +g𝐺 )
6 1 5 resvplusg ( 𝐴𝑉 → ( +g𝐺 ) = ( +g𝐻 ) )
7 6 oveqdr ( ( 𝐴𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝐻 ) 𝑦 ) )
8 2 4 7 cmnpropd ( 𝐴𝑉 → ( 𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd ) )