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

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