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

Metamath Proof Explorer

Theorem pwsval

Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsval.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsval.f ⊢ 𝐹 = ( Scalar ‘ 𝑅 )
Assertion pwsval ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )

Proof

Step Hyp Ref Expression
1 pwsval.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsval.f ⊢ 𝐹 = ( Scalar ‘ 𝑅 )
3 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
4 elex ⊢ ( 𝐼 ∈ 𝑊 → 𝐼 ∈ V )
5 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → 𝑟 = 𝑅 )
6 5 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( Scalar ‘ 𝑟 ) = ( Scalar ‘ 𝑅 ) )
7 6 2 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( Scalar ‘ 𝑟 ) = 𝐹 )
8 id ⊢ ( 𝑖 = 𝐼 → 𝑖 = 𝐼 )
9 sneq ⊢ ( 𝑟 = 𝑅 → { 𝑟 } = { 𝑅 } )
10 xpeq12 ⊢ ( ( 𝑖 = 𝐼 ∧ { 𝑟 } = { 𝑅 } ) → ( 𝑖 × { 𝑟 } ) = ( 𝐼 × { 𝑅 } ) )
11 8 9 10 syl2anr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( 𝑖 × { 𝑟 } ) = ( 𝐼 × { 𝑅 } ) )
12 7 11 oveq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑖 = 𝐼 ) → ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) ) = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
13 df-pws ⊢ ↑s = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( ( Scalar ‘ 𝑟 ) Xs ( 𝑖 × { 𝑟 } ) ) )
14 ovex ⊢ ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) ∈ V
15 12 13 14 ovmpoa ⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → ( 𝑅 ↑s 𝐼 ) = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
16 3 4 15 syl2an ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 ↑s 𝐼 ) = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )
17 1 16 eqtrid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )