Description: Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | resvbas.1 | ⊢ 𝐻 = ( 𝐺 ↾v 𝐴 ) | |
Assertion | resvcmn | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐺 ∈ CMnd ↔ 𝐻 ∈ CMnd ) ) |
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 ) ) |