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 
|- P = ( Poly1 ` R )
evl1deg1.2 
|- O = ( eval1 ` R )
evl1deg1.3 
|- K = ( Base ` R )
evl1deg1.4 
|- U = ( Base ` P )
evl1deg1.5 
|- .x. = ( .r ` R )
evl1deg1.6 
|- .+ = ( +g ` R )
evl1deg1.7 
|- C = ( coe1 ` M )
evl1deg1.8 
|- D = ( deg1 ` R )
evl1deg1.9 
|- A = ( C ` 1 )
evl1deg1.10 
|- B = ( C ` 0 )
evl1deg1.11 
|- ( ph -> R e. CRing )
evl1deg1.12 
|- ( ph -> M e. U )
evl1deg1.13 
|- ( ph -> ( D ` M ) = 1 )
evl1deg1.14 
|- ( ph -> X e. K )
Assertion evl1deg1 
|- ( ph -> ( ( O ` M ) ` X ) = ( ( A .x. X ) .+ B ) )

Proof

Step Hyp Ref Expression
1 evl1deg1.1 
 |-  P = ( Poly1 ` R )
2 evl1deg1.2 
 |-  O = ( eval1 ` R )
3 evl1deg1.3 
 |-  K = ( Base ` R )
4 evl1deg1.4 
 |-  U = ( Base ` P )
5 evl1deg1.5 
 |-  .x. = ( .r ` R )
6 evl1deg1.6 
 |-  .+ = ( +g ` R )
7 evl1deg1.7 
 |-  C = ( coe1 ` M )
8 evl1deg1.8 
 |-  D = ( deg1 ` R )
9 evl1deg1.9 
 |-  A = ( C ` 1 )
10 evl1deg1.10 
 |-  B = ( C ` 0 )
11 evl1deg1.11 
 |-  ( ph -> R e. CRing )
12 evl1deg1.12 
 |-  ( ph -> M e. U )
13 evl1deg1.13 
 |-  ( ph -> ( D ` M ) = 1 )
14 evl1deg1.14 
 |-  ( ph -> X e. K )
15 oveq2 
 |-  ( x = X -> ( k ( .g ` ( mulGrp ` R ) ) x ) = ( k ( .g ` ( mulGrp ` R ) ) X ) )
16 15 oveq2d 
 |-  ( x = X -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) x ) ) = ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) )
17 16 mpteq2dv 
 |-  ( x = X -> ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) x ) ) ) = ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) )
18 17 oveq2d 
 |-  ( x = X -> ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) x ) ) ) ) = ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) )
19 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
20 2 1 3 4 11 12 5 19 7 evl1fpws 
 |-  ( ph -> ( O ` M ) = ( x e. K |-> ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) x ) ) ) ) ) )
21 ovexd 
 |-  ( ph -> ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) e. _V )
22 18 20 14 21 fvmptd4 
 |-  ( ph -> ( ( O ` M ) ` X ) = ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 11 crngringd 
 |-  ( ph -> R e. Ring )
25 24 ringcmnd 
 |-  ( ph -> R e. CMnd )
26 nn0ex 
 |-  NN0 e. _V
27 26 a1i 
 |-  ( ph -> NN0 e. _V )
28 24 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> R e. Ring )
29 7 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ k e. NN0 ) -> ( C ` k ) e. K )
30 12 29 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( C ` k ) e. K )
31 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
32 31 3 mgpbas 
 |-  K = ( Base ` ( mulGrp ` R ) )
33 31 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
34 24 33 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
35 34 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( mulGrp ` R ) e. Mnd )
36 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
37 14 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> X e. K )
38 32 19 35 36 37 mulgnn0cld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k ( .g ` ( mulGrp ` R ) ) X ) e. K )
39 3 5 28 30 38 ringcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) e. K )
40 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
41 fveq2 
 |-  ( k = j -> ( C ` k ) = ( C ` j ) )
42 oveq1 
 |-  ( k = j -> ( k ( .g ` ( mulGrp ` R ) ) X ) = ( j ( .g ` ( mulGrp ` R ) ) X ) )
43 41 42 oveq12d 
 |-  ( k = j -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) )
44 breq1 
 |-  ( i = ( D ` M ) -> ( i < j <-> ( D ` M ) < j ) )
45 44 imbi1d 
 |-  ( i = ( D ` M ) -> ( ( i < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) <-> ( ( D ` M ) < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) ) )
46 45 ralbidv 
 |-  ( i = ( D ` M ) -> ( A. j e. NN0 ( i < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) <-> A. j e. NN0 ( ( D ` M ) < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) ) )
47 1nn0 
 |-  1 e. NN0
48 13 47 eqeltrdi 
 |-  ( ph -> ( D ` M ) e. NN0 )
49 12 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> M e. U )
50 simplr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> j e. NN0 )
51 simpr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( D ` M ) < j )
52 8 1 4 23 7 deg1lt 
 |-  ( ( M e. U /\ j e. NN0 /\ ( D ` M ) < j ) -> ( C ` j ) = ( 0g ` R ) )
53 49 50 51 52 syl3anc 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( C ` j ) = ( 0g ` R ) )
54 53 oveq1d 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( ( 0g ` R ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) )
55 24 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> R e. Ring )
56 55 33 syl 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( mulGrp ` R ) e. Mnd )
57 14 ad2antrr 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> X e. K )
58 32 19 56 50 57 mulgnn0cld 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( j ( .g ` ( mulGrp ` R ) ) X ) e. K )
59 3 5 23 55 58 ringlzd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( ( 0g ` R ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) )
60 54 59 eqtrd 
 |-  ( ( ( ph /\ j e. NN0 ) /\ ( D ` M ) < j ) -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) )
61 60 ex 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( D ` M ) < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) )
62 61 ralrimiva 
 |-  ( ph -> A. j e. NN0 ( ( D ` M ) < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) )
63 46 48 62 rspcedvdw 
 |-  ( ph -> E. i e. NN0 A. j e. NN0 ( i < j -> ( ( C ` j ) .x. ( j ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) ) )
64 40 39 43 63 mptnn0fsuppd 
 |-  ( ph -> ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) finSupp ( 0g ` R ) )
65 nn0disj01 
 |-  ( { 0 , 1 } i^i ( ZZ>= ` 2 ) ) = (/)
66 65 a1i 
 |-  ( ph -> ( { 0 , 1 } i^i ( ZZ>= ` 2 ) ) = (/) )
67 nn0split01 
 |-  NN0 = ( { 0 , 1 } u. ( ZZ>= ` 2 ) )
68 67 a1i 
 |-  ( ph -> NN0 = ( { 0 , 1 } u. ( ZZ>= ` 2 ) ) )
69 3 23 6 25 27 39 64 66 68 gsumsplit2 
 |-  ( ph -> ( R gsum ( k e. NN0 |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) = ( ( R gsum ( k e. { 0 , 1 } |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) ) )
70 0nn0 
 |-  0 e. NN0
71 70 a1i 
 |-  ( ph -> 0 e. NN0 )
72 47 a1i 
 |-  ( ph -> 1 e. NN0 )
73 0ne1 
 |-  0 =/= 1
74 73 a1i 
 |-  ( ph -> 0 =/= 1 )
75 7 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ 0 e. NN0 ) -> ( C ` 0 ) e. K )
76 12 70 75 sylancl 
 |-  ( ph -> ( C ` 0 ) e. K )
77 32 19 34 71 14 mulgnn0cld 
 |-  ( ph -> ( 0 ( .g ` ( mulGrp ` R ) ) X ) e. K )
78 3 5 24 76 77 ringcld 
 |-  ( ph -> ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) e. K )
79 7 4 1 3 coe1fvalcl 
 |-  ( ( M e. U /\ 1 e. NN0 ) -> ( C ` 1 ) e. K )
80 12 47 79 sylancl 
 |-  ( ph -> ( C ` 1 ) e. K )
81 32 19 34 72 14 mulgnn0cld 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` R ) ) X ) e. K )
82 3 5 24 80 81 ringcld 
 |-  ( ph -> ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) e. K )
83 fveq2 
 |-  ( k = 0 -> ( C ` k ) = ( C ` 0 ) )
84 oveq1 
 |-  ( k = 0 -> ( k ( .g ` ( mulGrp ` R ) ) X ) = ( 0 ( .g ` ( mulGrp ` R ) ) X ) )
85 83 84 oveq12d 
 |-  ( k = 0 -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) )
86 fveq2 
 |-  ( k = 1 -> ( C ` k ) = ( C ` 1 ) )
87 oveq1 
 |-  ( k = 1 -> ( k ( .g ` ( mulGrp ` R ) ) X ) = ( 1 ( .g ` ( mulGrp ` R ) ) X ) )
88 86 87 oveq12d 
 |-  ( k = 1 -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) )
89 3 6 85 88 gsumpr 
 |-  ( ( R e. CMnd /\ ( 0 e. NN0 /\ 1 e. NN0 /\ 0 =/= 1 ) /\ ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) e. K /\ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) e. K ) ) -> ( R gsum ( k e. { 0 , 1 } |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) = ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) )
90 25 71 72 74 78 82 89 syl132anc 
 |-  ( ph -> ( R gsum ( k e. { 0 , 1 } |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) = ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) )
91 12 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> M e. U )
92 2eluzge0 
 |-  2 e. ( ZZ>= ` 0 )
93 uzss 
 |-  ( 2 e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 2 ) C_ ( ZZ>= ` 0 ) )
94 92 93 ax-mp 
 |-  ( ZZ>= ` 2 ) C_ ( ZZ>= ` 0 )
95 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
96 94 95 sseqtrri 
 |-  ( ZZ>= ` 2 ) C_ NN0
97 96 a1i 
 |-  ( ph -> ( ZZ>= ` 2 ) C_ NN0 )
98 97 sselda 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. NN0 )
99 13 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( D ` M ) = 1 )
100 eluz2gt1 
 |-  ( k e. ( ZZ>= ` 2 ) -> 1 < k )
101 100 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 < k )
102 99 101 eqbrtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( D ` M ) < k )
103 8 1 4 23 7 deg1lt 
 |-  ( ( M e. U /\ k e. NN0 /\ ( D ` M ) < k ) -> ( C ` k ) = ( 0g ` R ) )
104 91 98 102 103 syl3anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( C ` k ) = ( 0g ` R ) )
105 104 oveq1d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( ( 0g ` R ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) )
106 24 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> R e. Ring )
107 106 33 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( mulGrp ` R ) e. Mnd )
108 14 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> X e. K )
109 32 19 107 98 108 mulgnn0cld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k ( .g ` ( mulGrp ` R ) ) X ) e. K )
110 3 5 23 106 109 ringlzd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 0g ` R ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) )
111 105 110 eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) = ( 0g ` R ) )
112 111 mpteq2dva 
 |-  ( ph -> ( k e. ( ZZ>= ` 2 ) |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) = ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) )
113 112 oveq2d 
 |-  ( ph -> ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) = ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) ) )
114 90 113 oveq12d 
 |-  ( ph -> ( ( R gsum ( k e. { 0 , 1 } |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) ) = ( ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) ) ) )
115 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
116 10 76 eqeltrid 
 |-  ( ph -> B e. K )
117 3 5 115 24 116 ringridmd 
 |-  ( ph -> ( B .x. ( 1r ` R ) ) = B )
118 117 oveq1d 
 |-  ( ph -> ( ( B .x. ( 1r ` R ) ) .+ ( A .x. X ) ) = ( B .+ ( A .x. X ) ) )
119 10 a1i 
 |-  ( ph -> B = ( C ` 0 ) )
120 31 115 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
121 32 120 19 mulg0 
 |-  ( X e. K -> ( 0 ( .g ` ( mulGrp ` R ) ) X ) = ( 1r ` R ) )
122 14 121 syl 
 |-  ( ph -> ( 0 ( .g ` ( mulGrp ` R ) ) X ) = ( 1r ` R ) )
123 122 eqcomd 
 |-  ( ph -> ( 1r ` R ) = ( 0 ( .g ` ( mulGrp ` R ) ) X ) )
124 119 123 oveq12d 
 |-  ( ph -> ( B .x. ( 1r ` R ) ) = ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) )
125 9 a1i 
 |-  ( ph -> A = ( C ` 1 ) )
126 32 19 mulg1 
 |-  ( X e. K -> ( 1 ( .g ` ( mulGrp ` R ) ) X ) = X )
127 14 126 syl 
 |-  ( ph -> ( 1 ( .g ` ( mulGrp ` R ) ) X ) = X )
128 127 eqcomd 
 |-  ( ph -> X = ( 1 ( .g ` ( mulGrp ` R ) ) X ) )
129 125 128 oveq12d 
 |-  ( ph -> ( A .x. X ) = ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) )
130 124 129 oveq12d 
 |-  ( ph -> ( ( B .x. ( 1r ` R ) ) .+ ( A .x. X ) ) = ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) )
131 9 80 eqeltrid 
 |-  ( ph -> A e. K )
132 3 5 24 131 14 ringcld 
 |-  ( ph -> ( A .x. X ) e. K )
133 3 6 ringcom 
 |-  ( ( R e. Ring /\ B e. K /\ ( A .x. X ) e. K ) -> ( B .+ ( A .x. X ) ) = ( ( A .x. X ) .+ B ) )
134 24 116 132 133 syl3anc 
 |-  ( ph -> ( B .+ ( A .x. X ) ) = ( ( A .x. X ) .+ B ) )
135 118 130 134 3eqtr3d 
 |-  ( ph -> ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) = ( ( A .x. X ) .+ B ) )
136 11 crnggrpd 
 |-  ( ph -> R e. Grp )
137 136 grpmndd 
 |-  ( ph -> R e. Mnd )
138 fvexd 
 |-  ( ph -> ( ZZ>= ` 2 ) e. _V )
139 23 gsumz 
 |-  ( ( R e. Mnd /\ ( ZZ>= ` 2 ) e. _V ) -> ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
140 137 138 139 syl2anc 
 |-  ( ph -> ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) ) = ( 0g ` R ) )
141 135 140 oveq12d 
 |-  ( ph -> ( ( ( ( C ` 0 ) .x. ( 0 ( .g ` ( mulGrp ` R ) ) X ) ) .+ ( ( C ` 1 ) .x. ( 1 ( .g ` ( mulGrp ` R ) ) X ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( 0g ` R ) ) ) ) = ( ( ( A .x. X ) .+ B ) .+ ( 0g ` R ) ) )
142 3 6 136 132 116 grpcld 
 |-  ( ph -> ( ( A .x. X ) .+ B ) e. K )
143 3 6 23 136 142 grpridd 
 |-  ( ph -> ( ( ( A .x. X ) .+ B ) .+ ( 0g ` R ) ) = ( ( A .x. X ) .+ B ) )
144 114 141 143 3eqtrd 
 |-  ( ph -> ( ( R gsum ( k e. { 0 , 1 } |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) .+ ( R gsum ( k e. ( ZZ>= ` 2 ) |-> ( ( C ` k ) .x. ( k ( .g ` ( mulGrp ` R ) ) X ) ) ) ) ) = ( ( A .x. X ) .+ B ) )
145 22 69 144 3eqtrd 
 |-  ( ph -> ( ( O ` M ) ` X ) = ( ( A .x. X ) .+ B ) )