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	syl5eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝑌 = ( 𝐹 Xs ( 𝐼 × { 𝑅 } ) ) )