Metamath Proof Explorer


Theorem pwscmn

Description: The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypothesis pwscmn.y 𝑌 = ( 𝑅s 𝐼 )
Assertion pwscmn ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → 𝑌 ∈ CMnd )

Proof

Step Hyp Ref Expression
1 pwscmn.y 𝑌 = ( 𝑅s 𝐼 )
2 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
3 1 2 pwsval ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
4 eqid ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
5 simpr ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → 𝐼𝑉 )
6 fvexd ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ V )
7 fconst6g ( 𝑅 ∈ CMnd → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ CMnd )
8 7 adantr ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ CMnd )
9 4 5 6 8 prdscmnd ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ CMnd )
10 3 9 eqeltrd ( ( 𝑅 ∈ CMnd ∧ 𝐼𝑉 ) → 𝑌 ∈ CMnd )