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 𝑌 = ( 𝑅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 ‘ 𝑌 ) )