Theorem pwsvscaval

Description: Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	pwsvscaval.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsvscaval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	pwsvscaval.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
	pwsvscaval.t	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
	pwsvscaval.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
	pwsvscaval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	pwsvscaval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	pwsvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	pwsvscaval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	pwsvscaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	pwsvscaval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	pwsvscaval	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwsvscaval.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsvscaval.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		pwsvscaval.s	⊢ · = ( ·𝑠 ‘ 𝑅 )
4		pwsvscaval.t	⊢ ∙ = ( ·𝑠 ‘ 𝑌 )
5		pwsvscaval.f	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
6		pwsvscaval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
7		pwsvscaval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
8		pwsvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
9		pwsvscaval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
10		pwsvscaval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11		pwsvscaval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
12	1 2 3 4 5 6 7 8 9 10	pwsvscafval	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) = ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) )
13	12	fveq1d	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	1 14 2 7 8 10	pwselbas	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
16	15	ffnd	⊢ ( 𝜑 → 𝑋 Fn 𝐼 )
17		eqidd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐼 ) → ( 𝑋 ‘ 𝐽 ) = ( 𝑋 ‘ 𝐽 ) )
18	8 9 16 17	ofc1	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐼 ) → ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )
19	11 18	mpdan	⊢ ( 𝜑 → ( ( ( 𝐼 × { 𝐴 } ) ∘f · 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )
20	13 19	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝐽 ) = ( 𝐴 · ( 𝑋 ‘ 𝐽 ) ) )