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

Metamath Proof Explorer

Theorem pwsval

Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsval.y 
|- Y = ( R ^s I )
pwsval.f 
|- F = ( Scalar ` R )
Assertion pwsval 
|- ( ( R e. V /\ I e. W ) -> Y = ( F Xs_ ( I X. { R } ) ) )

Proof

Step Hyp Ref Expression
1 pwsval.y 
 |-  Y = ( R ^s I )
2 pwsval.f 
 |-  F = ( Scalar ` R )
3 elex 
 |-  ( R e. V -> R e. _V )
4 elex 
 |-  ( I e. W -> I e. _V )
5 simpl 
 |-  ( ( r = R /\ i = I ) -> r = R )
6 5 fveq2d 
 |-  ( ( r = R /\ i = I ) -> ( Scalar ` r ) = ( Scalar ` R ) )
7 6 2 eqtr4di 
 |-  ( ( r = R /\ i = I ) -> ( Scalar ` r ) = F )
8 id 
 |-  ( i = I -> i = I )
9 sneq 
 |-  ( r = R -> { r } = { R } )
10 xpeq12 
 |-  ( ( i = I /\ { r } = { R } ) -> ( i X. { r } ) = ( I X. { R } ) )
11 8 9 10 syl2anr 
 |-  ( ( r = R /\ i = I ) -> ( i X. { r } ) = ( I X. { R } ) )
12 7 11 oveq12d 
 |-  ( ( r = R /\ i = I ) -> ( ( Scalar ` r ) Xs_ ( i X. { r } ) ) = ( F Xs_ ( I X. { R } ) ) )
13 df-pws 
 |-  ^s = ( r e. _V , i e. _V |-> ( ( Scalar ` r ) Xs_ ( i X. { r } ) ) )
14 ovex 
 |-  ( F Xs_ ( I X. { R } ) ) e. _V
15 12 13 14 ovmpoa 
 |-  ( ( R e. _V /\ I e. _V ) -> ( R ^s I ) = ( F Xs_ ( I X. { R } ) ) )
16 3 4 15 syl2an 
 |-  ( ( R e. V /\ I e. W ) -> ( R ^s I ) = ( F Xs_ ( I X. { R } ) ) )
17 1 16 eqtrid 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( F Xs_ ( I X. { R } ) ) )