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 ^s I )
Assertion pwsabl
|- ( ( R e. Abel /\ I e. V ) -> Y e. Abel )

Proof

Step Hyp Ref Expression
1 pwscmn.y
 |-  Y = ( R ^s I )
2 eqid
 |-  ( Scalar ` R ) = ( Scalar ` R )
3 1 2 pwsval
 |-  ( ( R e. Abel /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
4 eqid
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
5 simpr
 |-  ( ( R e. Abel /\ I e. V ) -> I e. V )
6 fvexd
 |-  ( ( R e. Abel /\ I e. V ) -> ( Scalar ` R ) e. _V )
7 fconst6g
 |-  ( R e. Abel -> ( I X. { R } ) : I --> Abel )
8 7 adantr
 |-  ( ( R e. Abel /\ I e. V ) -> ( I X. { R } ) : I --> Abel )
9 4 5 6 8 prdsabld
 |-  ( ( R e. Abel /\ I e. V ) -> ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) e. Abel )
10 3 9 eqeltrd
 |-  ( ( R e. Abel /\ I e. V ) -> Y e. Abel )