Metamath Proof Explorer

Theorem evladdval

Description: Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses evladdval.q ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
evladdval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
evladdval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evladdval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evladdval.g ⊢ ✚ = ( +g ‘ 𝑃 )
evladdval.f ⊢ + = ( +g ‘ 𝑆 )
evladdval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
evladdval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evladdval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
evladdval.m ⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
evladdval.n ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
Assertion evladdval ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 evladdval.q ⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2 evladdval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
3 evladdval.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
4 evladdval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 evladdval.g ⊢ ✚ = ( +g ‘ 𝑃 )
6 evladdval.f ⊢ + = ( +g ‘ 𝑆 )
7 evladdval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
8 evladdval.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 evladdval.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
10 evladdval.m ⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
11 evladdval.n ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
12 eqid ⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
13 1 3 2 12 evlrhm ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
14 7 8 13 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
15 rhmghm ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
16 14 15 syl ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
17 ghmgrp1 ⊢ ( 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑃 ∈ Grp )
18 16 17 syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
19 10 simpld ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
20 11 simpld ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
21 4 5 18 19 20 grpcld ⊢ ( 𝜑 → ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 )
22 eqid ⊢ ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
23 4 5 22 ghmlin ⊢ ( ( 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
24 16 19 20 23 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
25 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
26 ovexd ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
27 4 25 rhmf ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
28 14 27 syl ⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
29 28 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
30 28 20 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
31 12 25 8 26 29 30 6 22 pwsplusgval ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) )
32 24 31 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) )
33 32 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) )
34 12 3 25 8 26 29 pwselbas ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
35 34 ffnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) )
36 12 3 25 8 26 30 pwselbas ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
37 36 ffnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) )
38 fnfvof ⊢ ( ( ( ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) ∧ ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) ) ∧ ( ( 𝐾 ↑m 𝐼 ) ∈ V ∧ 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) ) → ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
39 35 37 26 9 38 syl22anc ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
40 10 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 )
41 11 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 )
42 40 41 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) = ( 𝑉 + 𝑊 ) )
43 33 39 42 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) )
44 21 43 jca ⊢ ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) ) )