prdsmulrfval

Description: Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	⊢ 𝑌 = ( 𝑆 X_s 𝑅 )
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		prdsmulrfval.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
10	1 2 3 4 5 6 7 8	prdsmulrval	⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐽 ) )
12		2fveq3	⊢ ( 𝑥 = 𝐽 → ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) = ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) )
13		fveq2	⊢ ( 𝑥 = 𝐽 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐽 ) )
14		fveq2	⊢ ( 𝑥 = 𝐽 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐽 ) )
15	12 13 14	oveq123d	⊢ ( 𝑥 = 𝐽 → ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝐽 ) ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
16		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17		ovex	⊢ ( ( 𝐹 ‘ 𝐽 ) ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) ∈ V
18	15 16 17	fvmpt	⊢ ( 𝐽 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( ( 𝐹 ‘ 𝐽 ) ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
19	9 18	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( ( 𝐹 ‘ 𝐽 ) ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )
20	11 19	eqtrd	⊢ ( 𝜑 → ( ( 𝐹 · 𝐺 ) ‘ 𝐽 ) = ( ( 𝐹 ‘ 𝐽 ) ( ._r ‘ ( 𝑅 ‘ 𝐽 ) ) ( 𝐺 ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem prdsmulrfval

Proof