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 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 ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )