Metamath Proof Explorer


Theorem evlsmulval

Description: Polynomial evaluation builder for multiplication. (Contributed by SN, 27-Jul-2024)

Ref Expression
Hypotheses evlsaddval.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
evlsaddval.p 𝑃 = ( 𝐼 mPoly 𝑈 )
evlsaddval.u 𝑈 = ( 𝑆s 𝑅 )
evlsaddval.k 𝐾 = ( Base ‘ 𝑆 )
evlsaddval.b 𝐵 = ( Base ‘ 𝑃 )
evlsaddval.i ( 𝜑𝐼𝑍 )
evlsaddval.s ( 𝜑𝑆 ∈ CRing )
evlsaddval.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evlsaddval.a ( 𝜑𝐴 ∈ ( 𝐾m 𝐼 ) )
evlsaddval.m ( 𝜑 → ( 𝑀𝐵 ∧ ( ( 𝑄𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
evlsaddval.n ( 𝜑 → ( 𝑁𝐵 ∧ ( ( 𝑄𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
evlsmulval.g = ( .r𝑃 )
evlsmulval.f · = ( .r𝑆 )
Assertion evlsmulval ( 𝜑 → ( ( 𝑀 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 evlsaddval.q 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsaddval.p 𝑃 = ( 𝐼 mPoly 𝑈 )
3 evlsaddval.u 𝑈 = ( 𝑆s 𝑅 )
4 evlsaddval.k 𝐾 = ( Base ‘ 𝑆 )
5 evlsaddval.b 𝐵 = ( Base ‘ 𝑃 )
6 evlsaddval.i ( 𝜑𝐼𝑍 )
7 evlsaddval.s ( 𝜑𝑆 ∈ CRing )
8 evlsaddval.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9 evlsaddval.a ( 𝜑𝐴 ∈ ( 𝐾m 𝐼 ) )
10 evlsaddval.m ( 𝜑 → ( 𝑀𝐵 ∧ ( ( 𝑄𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
11 evlsaddval.n ( 𝜑 → ( 𝑁𝐵 ∧ ( ( 𝑄𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
12 evlsmulval.g = ( .r𝑃 )
13 evlsmulval.f · = ( .r𝑆 )
14 eqid ( 𝑆s ( 𝐾m 𝐼 ) ) = ( 𝑆s ( 𝐾m 𝐼 ) )
15 1 2 3 14 4 evlsrhm ( ( 𝐼𝑍𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
16 6 7 8 15 syl3anc ( 𝜑𝑄 ∈ ( 𝑃 RingHom ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
17 rhmrcl1 ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆s ( 𝐾m 𝐼 ) ) ) → 𝑃 ∈ Ring )
18 16 17 syl ( 𝜑𝑃 ∈ Ring )
19 10 simpld ( 𝜑𝑀𝐵 )
20 11 simpld ( 𝜑𝑁𝐵 )
21 5 12 ringcl ( ( 𝑃 ∈ Ring ∧ 𝑀𝐵𝑁𝐵 ) → ( 𝑀 𝑁 ) ∈ 𝐵 )
22 18 19 20 21 syl3anc ( 𝜑 → ( 𝑀 𝑁 ) ∈ 𝐵 )
23 eqid ( .r ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) = ( .r ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) )
24 5 12 23 rhmmul ( ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆s ( 𝐾m 𝐼 ) ) ) ∧ 𝑀𝐵𝑁𝐵 ) → ( 𝑄 ‘ ( 𝑀 𝑁 ) ) = ( ( 𝑄𝑀 ) ( .r ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) ( 𝑄𝑁 ) ) )
25 16 19 20 24 syl3anc ( 𝜑 → ( 𝑄 ‘ ( 𝑀 𝑁 ) ) = ( ( 𝑄𝑀 ) ( .r ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) ( 𝑄𝑁 ) ) )
26 eqid ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) = ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) )
27 ovexd ( 𝜑 → ( 𝐾m 𝐼 ) ∈ V )
28 5 26 rhmf ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆s ( 𝐾m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
29 16 28 syl ( 𝜑𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
30 29 19 ffvelrnd ( 𝜑 → ( 𝑄𝑀 ) ∈ ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
31 29 20 ffvelrnd ( 𝜑 → ( 𝑄𝑁 ) ∈ ( Base ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) )
32 14 26 7 27 30 31 13 23 pwsmulrval ( 𝜑 → ( ( 𝑄𝑀 ) ( .r ‘ ( 𝑆s ( 𝐾m 𝐼 ) ) ) ( 𝑄𝑁 ) ) = ( ( 𝑄𝑀 ) ∘f · ( 𝑄𝑁 ) ) )
33 25 32 eqtrd ( 𝜑 → ( 𝑄 ‘ ( 𝑀 𝑁 ) ) = ( ( 𝑄𝑀 ) ∘f · ( 𝑄𝑁 ) ) )
34 33 fveq1d ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄𝑀 ) ∘f · ( 𝑄𝑁 ) ) ‘ 𝐴 ) )
35 14 4 26 7 27 30 pwselbas ( 𝜑 → ( 𝑄𝑀 ) : ( 𝐾m 𝐼 ) ⟶ 𝐾 )
36 35 ffnd ( 𝜑 → ( 𝑄𝑀 ) Fn ( 𝐾m 𝐼 ) )
37 14 4 26 7 27 31 pwselbas ( 𝜑 → ( 𝑄𝑁 ) : ( 𝐾m 𝐼 ) ⟶ 𝐾 )
38 37 ffnd ( 𝜑 → ( 𝑄𝑁 ) Fn ( 𝐾m 𝐼 ) )
39 fnfvof ( ( ( ( 𝑄𝑀 ) Fn ( 𝐾m 𝐼 ) ∧ ( 𝑄𝑁 ) Fn ( 𝐾m 𝐼 ) ) ∧ ( ( 𝐾m 𝐼 ) ∈ V ∧ 𝐴 ∈ ( 𝐾m 𝐼 ) ) ) → ( ( ( 𝑄𝑀 ) ∘f · ( 𝑄𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄𝑀 ) ‘ 𝐴 ) · ( ( 𝑄𝑁 ) ‘ 𝐴 ) ) )
40 36 38 27 9 39 syl22anc ( 𝜑 → ( ( ( 𝑄𝑀 ) ∘f · ( 𝑄𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄𝑀 ) ‘ 𝐴 ) · ( ( 𝑄𝑁 ) ‘ 𝐴 ) ) )
41 10 simprd ( 𝜑 → ( ( 𝑄𝑀 ) ‘ 𝐴 ) = 𝑉 )
42 11 simprd ( 𝜑 → ( ( 𝑄𝑁 ) ‘ 𝐴 ) = 𝑊 )
43 41 42 oveq12d ( 𝜑 → ( ( ( 𝑄𝑀 ) ‘ 𝐴 ) · ( ( 𝑄𝑁 ) ‘ 𝐴 ) ) = ( 𝑉 · 𝑊 ) )
44 34 40 43 3eqtrd ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) )
45 22 44 jca ( 𝜑 → ( ( 𝑀 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 · 𝑊 ) ) )