Metamath Proof Explorer


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 ( 𝜑 → ( 𝐹 · 𝐺 ) = ( 𝑥𝐼 ↦ ( 𝐹 ( ·𝑠 ‘ ( 𝑅𝑥 ) ) ( 𝐺𝑥 ) ) ) )