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 RAbelIVYAbel

Proof

Step Hyp Ref Expression
1 pwscmn.y Y=R𝑠I
2 eqid ScalarR=ScalarR
3 1 2 pwsval RAbelIVY=ScalarR𝑠I×R
4 eqid ScalarR𝑠I×R=ScalarR𝑠I×R
5 simpr RAbelIVIV
6 fvexd RAbelIVScalarRV
7 fconst6g RAbelI×R:IAbel
8 7 adantr RAbelIVI×R:IAbel
9 4 5 6 8 prdsabld RAbelIVScalarR𝑠I×RAbel
10 3 9 eqeltrd RAbelIVYAbel