Theorem prdsmulrval

Description: Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015)

	Ref	Expression
Hypotheses	prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
	prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	prdsmulrval.t	⊢ · = ( .r ‘ 𝑌 )
Assertion	prdsmulrval	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsbasmpt.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt.r	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
6		prdsplusgval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		prdsplusgval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
8		prdsmulrval.t	⊢ · = ( .r ‘ 𝑌 )
9		fnex	⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ V )
10	5 4 9	syl2anc	⊢ ( 𝜑 → 𝑅 ∈ V )
11	5	fndmd	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
12	1 3 10 2 11 8	prdsmulr	⊢ ( 𝜑 → · = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) ) )
13		fveq1	⊢ ( 𝑦 = 𝐹 → ( 𝑦 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14		fveq1	⊢ ( 𝑧 = 𝐺 → ( 𝑧 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
15	13 14	oveqan12d	⊢ ( ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) → ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
16	15	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17	16	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
18	4	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
19	12 17 6 7 18	ovmpod	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )