This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwssca

Description: The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses pwssca.y 
|- Y = ( R ^s I )
pwssca.s 
|- S = ( Scalar ` R )
Assertion pwssca 
|- ( ( R e. V /\ I e. W ) -> S = ( Scalar ` Y ) )

Proof

Step Hyp Ref Expression
1 pwssca.y 
 |-  Y = ( R ^s I )
2 pwssca.s 
 |-  S = ( Scalar ` R )
3 eqid 
 |-  ( S Xs_ ( I X. { R } ) ) = ( S Xs_ ( I X. { R } ) )
4 2 fvexi 
 |-  S e. _V
5 4 a1i 
 |-  ( ( R e. V /\ I e. W ) -> S e. _V )
6 simpr 
 |-  ( ( R e. V /\ I e. W ) -> I e. W )
7 snex 
 |-  { R } e. _V
8 xpexg 
 |-  ( ( I e. W /\ { R } e. _V ) -> ( I X. { R } ) e. _V )
9 6 7 8 sylancl 
 |-  ( ( R e. V /\ I e. W ) -> ( I X. { R } ) e. _V )
10 3 5 9 prdssca 
 |-  ( ( R e. V /\ I e. W ) -> S = ( Scalar ` ( S Xs_ ( I X. { R } ) ) ) )
11 1 2 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( S Xs_ ( I X. { R } ) ) )
12 11 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` Y ) = ( Scalar ` ( S Xs_ ( I X. { R } ) ) ) )
13 10 12 eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> S = ( Scalar ` Y ) )