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	syl5eq	|- ( ( R e. V /\ I e. W ) -> Y = ( F Xs_ ( I X. { R } ) ) )