Metamath Proof Explorer

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 fndm ⊢ ( 𝑅 Fn 𝐼 → dom 𝑅 = 𝐼 )
12 5 11 syl ⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
13 1 3 10 2 12 8 prdsmulr ⊢ ( 𝜑 → · = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) ) )
14 fveq1 ⊢ ( 𝑦 = 𝐹 → ( 𝑦 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 fveq1 ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16 14 15 oveqan12d ⊢ ( ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) → ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) )
18 17 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑦 = 𝐹 ∧ 𝑧 = 𝐺 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑦 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑧 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )
19 4 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
20 13 18 6 7 19 ovmpod ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐺 ‘ 𝑥 ) ) ) )