Metamath Proof Explorer

Theorem evl1deg3

Description: Evaluation of a univariate polynomial of degree 3. (Contributed by Thierry Arnoux, 14-Jun-2025)

Ref Expression
Hypotheses evl1deg1.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1deg1.2 ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1deg1.3 ⊢ 𝐾 = ( Base ‘ 𝑅 )
evl1deg1.4 ⊢ 𝑈 = ( Base ‘ 𝑃 )
evl1deg1.5 ⊢ · = ( .r ‘ 𝑅 )
evl1deg1.6 ⊢ + = ( +g ‘ 𝑅 )
evl1deg2.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
evl1deg3.f ⊢ 𝐹 = ( coe1 ‘ 𝑀 )
evl1deg3.e ⊢ 𝐸 = ( deg1 ‘ 𝑅 )
evl1deg3.a ⊢ 𝐴 = ( 𝐹 ‘ 3 )
evl1deg3.b ⊢ 𝐵 = ( 𝐹 ‘ 2 )
evl1deg3.c ⊢ 𝐶 = ( 𝐹 ‘ 1 )
evl1deg3.d ⊢ 𝐷 = ( 𝐹 ‘ 0 )
evl1deg3.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1deg3.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
evl1deg3.1 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑀 ) = 3 )
evl1deg3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion evl1deg3 ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 evl1deg1.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 evl1deg1.2 ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
3 evl1deg1.3 ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 evl1deg1.4 ⊢ 𝑈 = ( Base ‘ 𝑃 )
5 evl1deg1.5 ⊢ · = ( .r ‘ 𝑅 )
6 evl1deg1.6 ⊢ + = ( +g ‘ 𝑅 )
7 evl1deg2.p ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
8 evl1deg3.f ⊢ 𝐹 = ( coe1 ‘ 𝑀 )
9 evl1deg3.e ⊢ 𝐸 = ( deg1 ‘ 𝑅 )
10 evl1deg3.a ⊢ 𝐴 = ( 𝐹 ‘ 3 )
11 evl1deg3.b ⊢ 𝐵 = ( 𝐹 ‘ 2 )
12 evl1deg3.c ⊢ 𝐶 = ( 𝐹 ‘ 1 )
13 evl1deg3.d ⊢ 𝐷 = ( 𝐹 ‘ 0 )
14 evl1deg3.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
15 evl1deg3.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
16 evl1deg3.1 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑀 ) = 3 )
17 evl1deg3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
18 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ↑ 𝑥 ) = ( 𝑘 ↑ 𝑋 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) )
20 19 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) )
21 20 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
22 2 1 3 4 14 15 5 7 8 evl1fpws ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )
23 ovexd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ V )
24 21 22 17 23 fvmptd4 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
25 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
26 14 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
27 26 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
28 nn0ex ⊢ ℕ0 ∈ V
29 28 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
30 26 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
31 8 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐾 )
32 15 31 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐾 )
33 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
34 33 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
35 33 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
36 26 35 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
39 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
40 34 7 37 38 39 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐾 )
41 3 5 30 32 40 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐾 )
42 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
43 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
44 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ↑ 𝑋 ) = ( 𝑗 ↑ 𝑋 ) )
45 43 44 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) )
46 breq1 ⊢ ( 𝑖 = ( 𝐸 ‘ 𝑀 ) → ( 𝑖 < 𝑗 ↔ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) )
47 46 imbi1d ⊢ ( 𝑖 = ( 𝐸 ‘ 𝑀 ) → ( ( 𝑖 < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( 𝐸 ‘ 𝑀 ) < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ) )
48 47 ralbidv ⊢ ( 𝑖 = ( 𝐸 ‘ 𝑀 ) → ( ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑗 ∈ ℕ0 ( ( 𝐸 ‘ 𝑀 ) < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ) )
49 3nn0 ⊢ 3 ∈ ℕ0
50 49 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
51 16 50 eqeltrd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑀 ) ∈ ℕ0 )
52 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → 𝑀 ∈ 𝑈 )
53 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → 𝑗 ∈ ℕ0 )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( 𝐸 ‘ 𝑀 ) < 𝑗 )
55 9 1 4 25 8 deg1lt ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑗 ∈ ℕ0 ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( 𝐹 ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
56 52 53 54 55 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( 𝐹 ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
57 56 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑗 ↑ 𝑋 ) ) )
58 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → 𝑅 ∈ Ring )
59 58 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
60 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → 𝑋 ∈ 𝐾 )
61 34 7 59 53 60 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( 𝑗 ↑ 𝑋 ) ∈ 𝐾 )
62 3 5 25 58 61 ringlzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( ( 0g ‘ 𝑅 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
63 57 62 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐸 ‘ 𝑀 ) < 𝑗 ) → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
64 63 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐸 ‘ 𝑀 ) < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
65 64 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( ( 𝐸 ‘ 𝑀 ) < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
66 48 51 65 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐹 ‘ 𝑗 ) · ( 𝑗 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
67 42 41 45 66 mptnn0fsuppd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
68 fzouzdisj ⊢ ( ( 0 ..^ 4 ) ∩ ( ℤ≥ ‘ 4 ) ) = ∅
69 68 a1i ⊢ ( 𝜑 → ( ( 0 ..^ 4 ) ∩ ( ℤ≥ ‘ 4 ) ) = ∅ )
70 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
71 4nn0 ⊢ 4 ∈ ℕ0
72 71 70 eleqtri ⊢ 4 ∈ ( ℤ≥ ‘ 0 )
73 fzouzsplit ⊢ ( 4 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) ) )
74 72 73 ax-mp ⊢ ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) )
75 70 74 eqtri ⊢ ℕ0 = ( ( 0 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) )
76 75 a1i ⊢ ( 𝜑 → ℕ0 = ( ( 0 ..^ 4 ) ∪ ( ℤ≥ ‘ 4 ) ) )
77 3 25 6 27 29 41 67 69 76 gsumsplit2 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
78 fzofi ⊢ ( 0 ..^ 4 ) ∈ Fin
79 78 a1i ⊢ ( 𝜑 → ( 0 ..^ 4 ) ∈ Fin )
80 fzo0ssnn0 ⊢ ( 0 ..^ 4 ) ⊆ ℕ0
81 80 a1i ⊢ ( 𝜑 → ( 0 ..^ 4 ) ⊆ ℕ0 )
82 81 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 4 ) ) → 𝑘 ∈ ℕ0 )
83 82 41 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 4 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐾 )
84 0ne2 ⊢ 0 ≠ 2
85 1ne2 ⊢ 1 ≠ 2
86 0re ⊢ 0 ∈ ℝ
87 3pos ⊢ 0 < 3
88 86 87 ltneii ⊢ 0 ≠ 3
89 1re ⊢ 1 ∈ ℝ
90 1lt3 ⊢ 1 < 3
91 89 90 ltneii ⊢ 1 ≠ 3
92 disjpr2 ⊢ ( ( ( 0 ≠ 2 ∧ 1 ≠ 2 ) ∧ ( 0 ≠ 3 ∧ 1 ≠ 3 ) ) → ( { 0 , 1 } ∩ { 2 , 3 } ) = ∅ )
93 84 85 88 91 92 mp4an ⊢ ( { 0 , 1 } ∩ { 2 , 3 } ) = ∅
94 93 a1i ⊢ ( 𝜑 → ( { 0 , 1 } ∩ { 2 , 3 } ) = ∅ )
95 fzo0to42pr ⊢ ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } )
96 95 a1i ⊢ ( 𝜑 → ( 0 ..^ 4 ) = ( { 0 , 1 } ∪ { 2 , 3 } ) )
97 3 6 27 79 83 94 96 gsummptfidmsplit ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
98 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑀 ∈ 𝑈 )
99 uzss ⊢ ( 4 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 4 ) ⊆ ( ℤ≥ ‘ 0 ) )
100 72 99 ax-mp ⊢ ( ℤ≥ ‘ 4 ) ⊆ ( ℤ≥ ‘ 0 )
101 100 70 sseqtrri ⊢ ( ℤ≥ ‘ 4 ) ⊆ ℕ0
102 101 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 4 ) ⊆ ℕ0 )
103 102 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑘 ∈ ℕ0 )
104 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝐸 ‘ 𝑀 ) = 3 )
105 3p1e4 ⊢ ( 3 + 1 ) = 4
106 105 fveq2i ⊢ ( ℤ≥ ‘ ( 3 + 1 ) ) = ( ℤ≥ ‘ 4 )
107 106 eleq2i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ↔ 𝑘 ∈ ( ℤ≥ ‘ 4 ) )
108 3z ⊢ 3 ∈ ℤ
109 eluzp1l ⊢ ( ( 3 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) ) → 3 < 𝑘 )
110 108 109 mpan ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 3 + 1 ) ) → 3 < 𝑘 )
111 107 110 sylbir ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) → 3 < 𝑘 )
112 111 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → 3 < 𝑘 )
113 104 112 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝐸 ‘ 𝑀 ) < 𝑘 )
114 9 1 4 25 8 deg1lt ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐸 ‘ 𝑀 ) < 𝑘 ) → ( 𝐹 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
115 98 103 113 114 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
116 115 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑘 ↑ 𝑋 ) ) )
117 26 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑅 ∈ Ring )
118 117 35 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
119 17 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑋 ∈ 𝐾 )
120 34 7 118 103 119 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐾 )
121 3 5 25 117 120 ringlzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 0g ‘ 𝑅 ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
122 116 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
123 122 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) )
124 123 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) ) )
125 97 124 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) ) ) )
126 0nn0 ⊢ 0 ∈ ℕ0
127 126 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
128 1nn0 ⊢ 1 ∈ ℕ0
129 128 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
130 0ne1 ⊢ 0 ≠ 1
131 130 a1i ⊢ ( 𝜑 → 0 ≠ 1 )
132 8 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 0 ∈ ℕ0 ) → ( 𝐹 ‘ 0 ) ∈ 𝐾 )
133 15 126 132 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ 𝐾 )
134 34 7 36 127 17 mulgnn0cld ⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) ∈ 𝐾 )
135 3 5 26 133 134 ringcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) ∈ 𝐾 )
136 8 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 1 ∈ ℕ0 ) → ( 𝐹 ‘ 1 ) ∈ 𝐾 )
137 15 128 136 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) ∈ 𝐾 )
138 34 7 36 129 17 mulgnn0cld ⊢ ( 𝜑 → ( 1 ↑ 𝑋 ) ∈ 𝐾 )
139 3 5 26 137 138 ringcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ∈ 𝐾 )
140 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
141 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
142 140 141 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) )
143 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 1 ) )
144 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ↑ 𝑋 ) = ( 1 ↑ 𝑋 ) )
145 143 144 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) )
146 3 6 142 145 gsumpr ⊢ ( ( 𝑅 ∈ CMnd ∧ ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 0 ≠ 1 ) ∧ ( ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) ∈ 𝐾 ∧ ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ∈ 𝐾 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) + ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ) )
147 27 127 129 131 135 139 146 syl132anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) + ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ) )
148 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
149 13 133 eqeltrid ⊢ ( 𝜑 → 𝐷 ∈ 𝐾 )
150 3 5 148 26 149 ringridmd ⊢ ( 𝜑 → ( 𝐷 · ( 1r ‘ 𝑅 ) ) = 𝐷 )
151 150 oveq1d ⊢ ( 𝜑 → ( ( 𝐷 · ( 1r ‘ 𝑅 ) ) + ( 𝐶 · 𝑋 ) ) = ( 𝐷 + ( 𝐶 · 𝑋 ) ) )
152 13 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝐹 ‘ 0 ) )
153 33 148 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
154 34 153 7 mulg0 ⊢ ( 𝑋 ∈ 𝐾 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
155 17 154 syl ⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
156 155 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0 ↑ 𝑋 ) )
157 152 156 oveq12d ⊢ ( 𝜑 → ( 𝐷 · ( 1r ‘ 𝑅 ) ) = ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) )
158 12 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝐹 ‘ 1 ) )
159 34 7 mulg1 ⊢ ( 𝑋 ∈ 𝐾 → ( 1 ↑ 𝑋 ) = 𝑋 )
160 17 159 syl ⊢ ( 𝜑 → ( 1 ↑ 𝑋 ) = 𝑋 )
161 160 eqcomd ⊢ ( 𝜑 → 𝑋 = ( 1 ↑ 𝑋 ) )
162 158 161 oveq12d ⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) = ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) )
163 157 162 oveq12d ⊢ ( 𝜑 → ( ( 𝐷 · ( 1r ‘ 𝑅 ) ) + ( 𝐶 · 𝑋 ) ) = ( ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) + ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ) )
164 162 139 eqeltrd ⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ 𝐾 )
165 3 6 ringcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐷 ∈ 𝐾 ∧ ( 𝐶 · 𝑋 ) ∈ 𝐾 ) → ( 𝐷 + ( 𝐶 · 𝑋 ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
166 26 149 164 165 syl3anc ⊢ ( 𝜑 → ( 𝐷 + ( 𝐶 · 𝑋 ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
167 151 163 166 3eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 0 ) · ( 0 ↑ 𝑋 ) ) + ( ( 𝐹 ‘ 1 ) · ( 1 ↑ 𝑋 ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
168 147 167 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝐶 · 𝑋 ) + 𝐷 ) )
169 2nn0 ⊢ 2 ∈ ℕ0
170 169 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
171 2re ⊢ 2 ∈ ℝ
172 2lt3 ⊢ 2 < 3
173 171 172 ltneii ⊢ 2 ≠ 3
174 173 a1i ⊢ ( 𝜑 → 2 ≠ 3 )
175 8 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 2 ∈ ℕ0 ) → ( 𝐹 ‘ 2 ) ∈ 𝐾 )
176 15 169 175 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 2 ) ∈ 𝐾 )
177 11 176 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
178 34 7 36 170 17 mulgnn0cld ⊢ ( 𝜑 → ( 2 ↑ 𝑋 ) ∈ 𝐾 )
179 3 5 26 177 178 ringcld ⊢ ( 𝜑 → ( 𝐵 · ( 2 ↑ 𝑋 ) ) ∈ 𝐾 )
180 8 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 3 ∈ ℕ0 ) → ( 𝐹 ‘ 3 ) ∈ 𝐾 )
181 15 49 180 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 3 ) ∈ 𝐾 )
182 10 181 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
183 34 7 36 50 17 mulgnn0cld ⊢ ( 𝜑 → ( 3 ↑ 𝑋 ) ∈ 𝐾 )
184 3 5 26 182 183 ringcld ⊢ ( 𝜑 → ( 𝐴 · ( 3 ↑ 𝑋 ) ) ∈ 𝐾 )
185 fveq2 ⊢ ( 𝑘 = 2 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 2 ) )
186 185 11 eqtr4di ⊢ ( 𝑘 = 2 → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
187 oveq1 ⊢ ( 𝑘 = 2 → ( 𝑘 ↑ 𝑋 ) = ( 2 ↑ 𝑋 ) )
188 186 187 oveq12d ⊢ ( 𝑘 = 2 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( 𝐵 · ( 2 ↑ 𝑋 ) ) )
189 fveq2 ⊢ ( 𝑘 = 3 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 3 ) )
190 189 10 eqtr4di ⊢ ( 𝑘 = 3 → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
191 oveq1 ⊢ ( 𝑘 = 3 → ( 𝑘 ↑ 𝑋 ) = ( 3 ↑ 𝑋 ) )
192 190 191 oveq12d ⊢ ( 𝑘 = 3 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( 𝐴 · ( 3 ↑ 𝑋 ) ) )
193 3 6 188 192 gsumpr ⊢ ( ( 𝑅 ∈ CMnd ∧ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 2 ≠ 3 ) ∧ ( ( 𝐵 · ( 2 ↑ 𝑋 ) ) ∈ 𝐾 ∧ ( 𝐴 · ( 3 ↑ 𝑋 ) ) ∈ 𝐾 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝐵 · ( 2 ↑ 𝑋 ) ) + ( 𝐴 · ( 3 ↑ 𝑋 ) ) ) )
194 27 170 50 174 179 184 193 syl132anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝐵 · ( 2 ↑ 𝑋 ) ) + ( 𝐴 · ( 3 ↑ 𝑋 ) ) ) )
195 3 6 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ ( 𝐵 · ( 2 ↑ 𝑋 ) ) ∈ 𝐾 ∧ ( 𝐴 · ( 3 ↑ 𝑋 ) ) ∈ 𝐾 ) → ( ( 𝐵 · ( 2 ↑ 𝑋 ) ) + ( 𝐴 · ( 3 ↑ 𝑋 ) ) ) = ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) )
196 27 179 184 195 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 · ( 2 ↑ 𝑋 ) ) + ( 𝐴 · ( 3 ↑ 𝑋 ) ) ) = ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) )
197 194 196 eqtrd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) )
198 168 197 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) + ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) ) )
199 14 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
200 3 6 199 164 149 grpcld ⊢ ( 𝜑 → ( ( 𝐶 · 𝑋 ) + 𝐷 ) ∈ 𝐾 )
201 3 6 199 184 179 grpcld ⊢ ( 𝜑 → ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) ∈ 𝐾 )
202 3 6 cmncom ⊢ ( ( 𝑅 ∈ CMnd ∧ ( ( 𝐶 · 𝑋 ) + 𝐷 ) ∈ 𝐾 ∧ ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) ∈ 𝐾 ) → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) + ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
203 27 200 201 202 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝑋 ) + 𝐷 ) + ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
204 198 203 eqtrd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
205 199 grpmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
206 fvexd ⊢ ( 𝜑 → ( ℤ≥ ‘ 4 ) ∈ V )
207 25 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ℤ≥ ‘ 4 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
208 205 206 207 syl2anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
209 204 208 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ { 2 , 3 } ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( 0g ‘ 𝑅 ) ) ) ) = ( ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) + ( 0g ‘ 𝑅 ) ) )
210 3 6 199 201 200 grpcld ⊢ ( 𝜑 → ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ∈ 𝐾 )
211 3 6 25 199 210 grpridd ⊢ ( 𝜑 → ( ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) + ( 0g ‘ 𝑅 ) ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
212 125 209 211 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 4 ) ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )
213 24 77 212 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( ( ( 𝐴 · ( 3 ↑ 𝑋 ) ) + ( 𝐵 · ( 2 ↑ 𝑋 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) )