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 ) )