Theorem prdsvscafval

Description: Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsvscaval.t	⊢ · = ( ·𝑠 ‘ 𝑌 )
	prdsvscaval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	prdsvscaval.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsvscaval.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsvscaval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
	prdsvscaval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	prdsvscafval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	prdsvscafval	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsvscaval.t	⊢ · = ( ·𝑠 ‘ 𝑌 )
4		prdsvscaval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		prdsvscaval.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
6		prdsvscaval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		prdsvscaval.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
8		prdsvscaval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
9		prdsvscaval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		prdsvscafval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
11	1 2 3 4 5 6 7 8 9	prdsvscaval	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
12		2fveq3	⊢ ( 𝑥 = 𝐽 → ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) )
13		eqidd	⊢ ( 𝑥 = 𝐽 → 𝐹 = 𝐹 )
14		fveq2	⊢ ( 𝑥 = 𝐽 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐽 ) )
15	12 13 14	oveq123d	⊢ ( 𝑥 = 𝐽 → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐽 ) → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
17		ovexd	⊢ ( 𝜑 → ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) ∈ V )
18	11 16 10 17	fvmptd	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )