This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evl1deg2

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