Metamath Proof Explorer

Theorem evl1deg1

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

Ref Expression
Hypotheses evl1deg1.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
evl1deg1.2 ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
evl1deg1.3 ⊢ 𝐾 = ( Base ‘ 𝑅 )
evl1deg1.4 ⊢ 𝑈 = ( Base ‘ 𝑃 )
evl1deg1.5 ⊢ · = ( .r ‘ 𝑅 )
evl1deg1.6 ⊢ + = ( +g ‘ 𝑅 )
evl1deg1.7 ⊢ 𝐶 = ( coe1 ‘ 𝑀 )
evl1deg1.8 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
evl1deg1.9 ⊢ 𝐴 = ( 𝐶 ‘ 1 )
evl1deg1.10 ⊢ 𝐵 = ( 𝐶 ‘ 0 )
evl1deg1.11 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evl1deg1.12 ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
evl1deg1.13 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = 1 )
evl1deg1.14 ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion evl1deg1 ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )

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 evl1deg1.7 ⊢ 𝐶 = ( coe1 ‘ 𝑀 )
8 evl1deg1.8 ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
9 evl1deg1.9 ⊢ 𝐴 = ( 𝐶 ‘ 1 )
10 evl1deg1.10 ⊢ 𝐵 = ( 𝐶 ‘ 0 )
11 evl1deg1.11 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
12 evl1deg1.12 ⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
13 evl1deg1.13 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) = 1 )
14 evl1deg1.14 ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
15 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) = ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
16 15 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) = ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
17 16 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) )
19 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
20 2 1 3 4 11 12 5 19 7 evl1fpws ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑥 ) ) ) ) ) )
21 ovexd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ∈ V )
22 18 20 14 21 fvmptd4 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) )
23 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
24 11 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
25 24 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
26 nn0ex ⊢ ℕ0 ∈ V
27 26 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
28 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
29 7 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 ‘ 𝑘 ) ∈ 𝐾 )
30 12 29 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 ‘ 𝑘 ) ∈ 𝐾 )
31 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
32 31 3 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
33 31 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
34 24 33 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
37 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
38 32 19 35 36 37 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐾 )
39 3 5 28 30 38 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ 𝐾 )
40 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
41 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑗 ) )
42 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
43 41 42 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
44 breq1 ⊢ ( 𝑖 = ( 𝐷 ‘ 𝑀 ) → ( 𝑖 < 𝑗 ↔ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) )
45 44 imbi1d ⊢ ( 𝑖 = ( 𝐷 ‘ 𝑀 ) → ( ( 𝑖 < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ↔ ( ( 𝐷 ‘ 𝑀 ) < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ) )
46 45 ralbidv ⊢ ( 𝑖 = ( 𝐷 ‘ 𝑀 ) → ( ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑗 ∈ ℕ0 ( ( 𝐷 ‘ 𝑀 ) < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) ) )
47 1nn0 ⊢ 1 ∈ ℕ0
48 13 47 eqeltrdi ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑀 ) ∈ ℕ0 )
49 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → 𝑀 ∈ 𝑈 )
50 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → 𝑗 ∈ ℕ0 )
51 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( 𝐷 ‘ 𝑀 ) < 𝑗 )
52 8 1 4 23 7 deg1lt ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑗 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( 𝐶 ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
53 49 50 51 52 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( 𝐶 ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
54 53 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
55 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → 𝑅 ∈ Ring )
56 55 33 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
57 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → 𝑋 ∈ 𝐾 )
58 32 19 56 50 57 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐾 )
59 3 5 23 55 58 ringlzd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( ( 0g ‘ 𝑅 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
60 54 59 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐷 ‘ 𝑀 ) < 𝑗 ) → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
61 60 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐷 ‘ 𝑀 ) < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
62 61 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( ( 𝐷 ‘ 𝑀 ) < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
63 46 48 62 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐶 ‘ 𝑗 ) · ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) ) )
64 40 39 43 63 mptnn0fsuppd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
65 nn0disj01 ⊢ ( { 0 , 1 } ∩ ( ℤ≥ ‘ 2 ) ) = ∅
66 65 a1i ⊢ ( 𝜑 → ( { 0 , 1 } ∩ ( ℤ≥ ‘ 2 ) ) = ∅ )
67 nn0split01 ⊢ ℕ0 = ( { 0 , 1 } ∪ ( ℤ≥ ‘ 2 ) )
68 67 a1i ⊢ ( 𝜑 → ℕ0 = ( { 0 , 1 } ∪ ( ℤ≥ ‘ 2 ) ) )
69 3 23 6 25 27 39 64 66 68 gsumsplit2 ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ) )
70 0nn0 ⊢ 0 ∈ ℕ0
71 70 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
72 47 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
73 0ne1 ⊢ 0 ≠ 1
74 73 a1i ⊢ ( 𝜑 → 0 ≠ 1 )
75 7 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 0 ∈ ℕ0 ) → ( 𝐶 ‘ 0 ) ∈ 𝐾 )
76 12 70 75 sylancl ⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) ∈ 𝐾 )
77 32 19 34 71 14 mulgnn0cld ⊢ ( 𝜑 → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐾 )
78 3 5 24 76 77 ringcld ⊢ ( 𝜑 → ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ 𝐾 )
79 7 4 1 3 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 1 ∈ ℕ0 ) → ( 𝐶 ‘ 1 ) ∈ 𝐾 )
80 12 47 79 sylancl ⊢ ( 𝜑 → ( 𝐶 ‘ 1 ) ∈ 𝐾 )
81 32 19 34 72 14 mulgnn0cld ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐾 )
82 3 5 24 80 81 ringcld ⊢ ( 𝜑 → ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ 𝐾 )
83 fveq2 ⊢ ( 𝑘 = 0 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 0 ) )
84 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
85 83 84 oveq12d ⊢ ( 𝑘 = 0 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
86 fveq2 ⊢ ( 𝑘 = 1 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 1 ) )
87 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
88 86 87 oveq12d ⊢ ( 𝑘 = 1 → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
89 3 6 85 88 gsumpr ⊢ ( ( 𝑅 ∈ CMnd ∧ ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 0 ≠ 1 ) ∧ ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ 𝐾 ∧ ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ∈ 𝐾 ) ) → ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) = ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) )
90 25 71 72 74 78 82 89 syl132anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) = ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) )
91 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑀 ∈ 𝑈 )
92 2eluzge0 ⊢ 2 ∈ ( ℤ≥ ‘ 0 )
93 uzss ⊢ ( 2 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 0 ) )
94 92 93 ax-mp ⊢ ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 0 )
95 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
96 94 95 sseqtrri ⊢ ( ℤ≥ ‘ 2 ) ⊆ ℕ0
97 96 a1i ⊢ ( 𝜑 → ( ℤ≥ ‘ 2 ) ⊆ ℕ0 )
98 97 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑘 ∈ ℕ0 )
99 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐷 ‘ 𝑀 ) = 1 )
100 eluz2gt1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑘 )
101 100 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝑘 )
102 99 101 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐷 ‘ 𝑀 ) < 𝑘 )
103 8 1 4 23 7 deg1lt ⊢ ( ( 𝑀 ∈ 𝑈 ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑀 ) < 𝑘 ) → ( 𝐶 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
104 91 98 102 103 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐶 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
105 104 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
106 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑅 ∈ Ring )
107 106 33 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
108 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑋 ∈ 𝐾 )
109 32 19 107 98 108 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐾 )
110 3 5 23 106 109 ringlzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 0g ‘ 𝑅 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
111 105 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
112 111 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) )
113 112 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) ) )
114 90 113 oveq12d ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ) = ( ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) ) ) )
115 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
116 10 76 eqeltrid ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
117 3 5 115 24 116 ringridmd ⊢ ( 𝜑 → ( 𝐵 · ( 1r ‘ 𝑅 ) ) = 𝐵 )
118 117 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 · ( 1r ‘ 𝑅 ) ) + ( 𝐴 · 𝑋 ) ) = ( 𝐵 + ( 𝐴 · 𝑋 ) ) )
119 10 a1i ⊢ ( 𝜑 → 𝐵 = ( 𝐶 ‘ 0 ) )
120 31 115 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
121 32 120 19 mulg0 ⊢ ( 𝑋 ∈ 𝐾 → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
122 14 121 syl ⊢ ( 𝜑 → ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = ( 1r ‘ 𝑅 ) )
123 122 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
124 119 123 oveq12d ⊢ ( 𝜑 → ( 𝐵 · ( 1r ‘ 𝑅 ) ) = ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
125 9 a1i ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ‘ 1 ) )
126 32 19 mulg1 ⊢ ( 𝑋 ∈ 𝐾 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = 𝑋 )
127 14 126 syl ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) = 𝑋 )
128 127 eqcomd ⊢ ( 𝜑 → 𝑋 = ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) )
129 125 128 oveq12d ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) = ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) )
130 124 129 oveq12d ⊢ ( 𝜑 → ( ( 𝐵 · ( 1r ‘ 𝑅 ) ) + ( 𝐴 · 𝑋 ) ) = ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) )
131 9 80 eqeltrid ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
132 3 5 24 131 14 ringcld ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝐾 )
133 3 6 ringcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝐾 ∧ ( 𝐴 · 𝑋 ) ∈ 𝐾 ) → ( 𝐵 + ( 𝐴 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
134 24 116 132 133 syl3anc ⊢ ( 𝜑 → ( 𝐵 + ( 𝐴 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
135 118 130 134 3eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
136 11 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
137 136 grpmndd ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
138 fvexd ⊢ ( 𝜑 → ( ℤ≥ ‘ 2 ) ∈ V )
139 23 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ℤ≥ ‘ 2 ) ∈ V ) → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
140 137 138 139 syl2anc ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑅 ) )
141 135 140 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐶 ‘ 0 ) · ( 0 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) + ( ( 𝐶 ‘ 1 ) · ( 1 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( 0g ‘ 𝑅 ) ) ) ) = ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) + ( 0g ‘ 𝑅 ) ) )
142 3 6 136 132 116 grpcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ 𝐾 )
143 3 6 23 136 142 grpridd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) + ( 0g ‘ 𝑅 ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
144 114 141 143 3eqtrd ⊢ ( 𝜑 → ( ( 𝑅 Σg ( 𝑘 ∈ { 0 , 1 } ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) + ( 𝑅 Σg ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↦ ( ( 𝐶 ‘ 𝑘 ) · ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑋 ) ) ) ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
145 22 69 144 3eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )