Theorem prdsvscaval

Description: Scalar multiplication in a structure product is pointwise. (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	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	prdsvscaval	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )

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		fnex	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
11	7 6 10	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ V )
12	7	fndmd	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
13	1 5 11 2 12 4 3	prdsvsca	⊢ ( 𝜑 → · = ( 𝑦 ∈ 𝐾 , 𝑧 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) ) )
14		id	⊢ ( 𝑦 = 𝐹 → 𝑦 = 𝐹 )
15		fveq1	⊢ ( 𝑧 = 𝐺 → ( 𝑧 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16	14 15	oveqan12d	⊢ ( ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) → ( 𝑦 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( 𝑦 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
18	17	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
19	6	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
20	13 18 8 9 19	ovmpod	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )