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 Y = R 𝑠 I
Assertion pwscmn R CMnd I V Y CMnd

Proof

Step Hyp Ref Expression
1 pwscmn.y Y = R 𝑠 I
2 eqid Scalar R = Scalar R
3 1 2 pwsval R CMnd I V Y = Scalar R 𝑠 I × R
4 eqid Scalar R 𝑠 I × R = Scalar R 𝑠 I × R
5 simpr R CMnd I V I V
6 fvexd R CMnd I V Scalar R V
7 fconst6g R CMnd I × R : I CMnd
8 7 adantr R CMnd I V I × R : I CMnd
9 4 5 6 8 prdscmnd R CMnd I V Scalar R 𝑠 I × R CMnd
10 3 9 eqeltrd R CMnd I V Y CMnd