Theorem pwssca

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

	Ref	Expression
Hypotheses	pwssca.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwssca.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
Assertion	pwssca	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑆 = ( Scalar ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		pwssca.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwssca.s	⊢ 𝑆 = ( Scalar ‘ 𝑅 )
3		eqid	⊢ ( 𝑆 Xs ( 𝐼 × { 𝑅 } ) ) = ( 𝑆 Xs ( 𝐼 × { 𝑅 } ) )
4	2	fvexi	⊢ 𝑆 ∈ V
5	4	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑆 ∈ V )
6		simpr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐼 ∈ 𝑊 )
7		snex	⊢ { 𝑅 } ∈ V
8		xpexg	⊢ ( ( 𝐼 ∈ 𝑊 ∧ { 𝑅 } ∈ V ) → ( 𝐼 × { 𝑅 } ) ∈ V )
9	6 7 8	sylancl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 𝑅 } ) ∈ V )
10	3 5 9	prdssca	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑆 = ( Scalar ‘ ( 𝑆 Xs ( 𝐼 × { 𝑅 } ) ) ) )
11	1 2	pwsval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( 𝑆 Xs ( 𝐼 × { 𝑅 } ) ) )
12	11	fveq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( Scalar ‘ 𝑌 ) = ( Scalar ‘ ( 𝑆 Xs ( 𝐼 × { 𝑅 } ) ) ) )
13	10 12	eqtr4d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑆 = ( Scalar ‘ 𝑌 ) )