Metamath Proof Explorer


Theorem pwsabl

Description: The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015)

Ref Expression
Hypothesis pwscmn.y Y = R 𝑠 I
Assertion pwsabl R Abel I V Y Abel

Proof

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