Metamath Proof Explorer

Theorem aks6d1c5lem1

Description: Lemma for claim 5, evaluate the linear factor at -c to get a root. (Contributed by metakunt, 5-May-2025)

Ref Expression
Hypotheses aks6d1p5.1 
|- ( ph -> K e. Field )
aks6d1p5.2 
|- ( ph -> P e. Prime )
aks6d1c5.3 
|- P = ( chr ` K )
aks6d1c5.4 
|- ( ph -> A e. NN0 )
aks6d1c5.5 
|- ( ph -> A < P )
aks6d1c5.6 
|- X = ( var1 ` K )
aks6d1c5.7 
|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
aks6d1c5.8 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c5p1.1 
|- ( ph -> B e. ( 0 ... A ) )
aks6d1c5p1.2 
|- ( ph -> C e. ( 0 ... A ) )
Assertion aks6d1c5lem1 
|- ( ph -> ( B = C <-> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( 0g ` K ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 
 |-  ( ph -> K e. Field )
2 aks6d1p5.2 
 |-  ( ph -> P e. Prime )
3 aks6d1c5.3 
 |-  P = ( chr ` K )
4 aks6d1c5.4 
 |-  ( ph -> A e. NN0 )
5 aks6d1c5.5 
 |-  ( ph -> A < P )
6 aks6d1c5.6 
 |-  X = ( var1 ` K )
7 aks6d1c5.7 
 |-  .^ = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
8 aks6d1c5.8 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
9 aks6d1c5p1.1 
 |-  ( ph -> B e. ( 0 ... A ) )
10 aks6d1c5p1.2 
 |-  ( ph -> C e. ( 0 ... A ) )
11 zringplusg 
 |-  + = ( +g ` ZZring )
12 11 eqcomi 
 |-  ( +g ` ZZring ) = +
13 12 a1i 
 |-  ( ph -> ( +g ` ZZring ) = + )
14 13 oveqd 
 |-  ( ph -> ( ( 0 - C ) ( +g ` ZZring ) B ) = ( ( 0 - C ) + B ) )
15 0cnd 
 |-  ( ph -> 0 e. CC )
16 10 elfzelzd 
 |-  ( ph -> C e. ZZ )
17 16 zcnd 
 |-  ( ph -> C e. CC )
18 9 elfzelzd 
 |-  ( ph -> B e. ZZ )
19 18 zcnd 
 |-  ( ph -> B e. CC )
20 15 17 19 subadd23d 
 |-  ( ph -> ( ( 0 - C ) + B ) = ( 0 + ( B - C ) ) )
21 19 17 subcld 
 |-  ( ph -> ( B - C ) e. CC )
22 21 addlidd 
 |-  ( ph -> ( 0 + ( B - C ) ) = ( B - C ) )
23 20 22 eqtrd 
 |-  ( ph -> ( ( 0 - C ) + B ) = ( B - C ) )
24 14 23 eqtrd 
 |-  ( ph -> ( ( 0 - C ) ( +g ` ZZring ) B ) = ( B - C ) )
25 24 fveq2d 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( ( ZRHom ` K ) ` ( B - C ) ) )
26 25 eqeq1d 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( 0g ` K ) <-> ( ( ZRHom ` K ) ` ( B - C ) ) = ( 0g ` K ) ) )
27 2 adantr 
 |-  ( ( ph /\ B = C ) -> P e. Prime )
28 prmnn 
 |-  ( P e. Prime -> P e. NN )
29 27 28 syl 
 |-  ( ( ph /\ B = C ) -> P e. NN )
30 29 nnzd 
 |-  ( ( ph /\ B = C ) -> P e. ZZ )
31 dvds0 
 |-  ( P e. ZZ -> P || 0 )
32 30 31 syl 
 |-  ( ( ph /\ B = C ) -> P || 0 )
33 19 adantr 
 |-  ( ( ph /\ B = C ) -> B e. CC )
34 33 subidd 
 |-  ( ( ph /\ B = C ) -> ( B - B ) = 0 )
35 34 eqcomd 
 |-  ( ( ph /\ B = C ) -> 0 = ( B - B ) )
36 simpr 
 |-  ( ( ph /\ B = C ) -> B = C )
37 36 oveq2d 
 |-  ( ( ph /\ B = C ) -> ( B - B ) = ( B - C ) )
38 35 37 eqtrd 
 |-  ( ( ph /\ B = C ) -> 0 = ( B - C ) )
39 32 38 breqtrd 
 |-  ( ( ph /\ B = C ) -> P || ( B - C ) )
40 39 ex 
 |-  ( ph -> ( B = C -> P || ( B - C ) ) )
41 2 28 syl 
 |-  ( ph -> P e. NN )
42 41 adantr 
 |-  ( ( ph /\ -. B = C ) -> P e. NN )
43 42 adantr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> P e. NN )
44 1zzd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 1 e. ZZ )
45 43 nnzd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> P e. ZZ )
46 45 44 zsubcld 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( P - 1 ) e. ZZ )
47 18 16 zsubcld 
 |-  ( ph -> ( B - C ) e. ZZ )
48 47 ad2antrr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) e. ZZ )
49 1e0p1 
 |-  1 = ( 0 + 1 )
50 49 a1i 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 1 = ( 0 + 1 ) )
51 simpr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> C < B )
52 16 zred 
 |-  ( ph -> C e. RR )
53 52 adantr 
 |-  ( ( ph /\ -. B = C ) -> C e. RR )
54 53 adantr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> C e. RR )
55 18 zred 
 |-  ( ph -> B e. RR )
56 55 adantr 
 |-  ( ( ph /\ -. B = C ) -> B e. RR )
57 56 adantr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> B e. RR )
58 54 57 posdifd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( C < B <-> 0 < ( B - C ) ) )
59 51 58 mpbid 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 0 < ( B - C ) )
60 0zd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 0 e. ZZ )
61 60 48 zltp1led 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( 0 < ( B - C ) <-> ( 0 + 1 ) <_ ( B - C ) ) )
62 59 61 mpbid 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( 0 + 1 ) <_ ( B - C ) )
63 50 62 eqbrtrd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 1 <_ ( B - C ) )
64 48 zred 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) e. RR )
65 43 nnred 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> P e. RR )
66 elfzle1 
 |-  ( C e. ( 0 ... A ) -> 0 <_ C )
67 10 66 syl 
 |-  ( ph -> 0 <_ C )
68 67 adantr 
 |-  ( ( ph /\ -. B = C ) -> 0 <_ C )
69 68 adantr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> 0 <_ C )
70 57 54 subge02d 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( 0 <_ C <-> ( B - C ) <_ B ) )
71 69 70 mpbid 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) <_ B )
72 4 nn0red 
 |-  ( ph -> A e. RR )
73 41 nnred 
 |-  ( ph -> P e. RR )
74 elfzle2 
 |-  ( B e. ( 0 ... A ) -> B <_ A )
75 9 74 syl 
 |-  ( ph -> B <_ A )
76 55 72 73 75 5 lelttrd 
 |-  ( ph -> B < P )
77 76 adantr 
 |-  ( ( ph /\ -. B = C ) -> B < P )
78 77 adantr 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> B < P )
79 64 57 65 71 78 lelttrd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) < P )
80 48 45 zltlem1d 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( ( B - C ) < P <-> ( B - C ) <_ ( P - 1 ) ) )
81 79 80 mpbid 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) <_ ( P - 1 ) )
82 44 46 48 63 81 elfzd 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> ( B - C ) e. ( 1 ... ( P - 1 ) ) )
83 fzm1ndvds 
 |-  ( ( P e. NN /\ ( B - C ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( B - C ) )
84 43 82 83 syl2anc 
 |-  ( ( ( ph /\ -. B = C ) /\ C < B ) -> -. P || ( B - C ) )
85 simpll 
 |-  ( ( ( ph /\ -. B = C ) /\ -. C < B ) -> ph )
86 axlttri 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B < C <-> -. ( B = C \/ C < B ) ) )
87 55 52 86 syl2anc 
 |-  ( ph -> ( B < C <-> -. ( B = C \/ C < B ) ) )
88 ioran 
 |-  ( -. ( B = C \/ C < B ) <-> ( -. B = C /\ -. C < B ) )
89 88 a1i 
 |-  ( ph -> ( -. ( B = C \/ C < B ) <-> ( -. B = C /\ -. C < B ) ) )
90 87 89 bitr2d 
 |-  ( ph -> ( ( -. B = C /\ -. C < B ) <-> B < C ) )
91 90 biimpd 
 |-  ( ph -> ( ( -. B = C /\ -. C < B ) -> B < C ) )
92 91 imp 
 |-  ( ( ph /\ ( -. B = C /\ -. C < B ) ) -> B < C )
93 92 anassrs 
 |-  ( ( ( ph /\ -. B = C ) /\ -. C < B ) -> B < C )
94 85 93 jca 
 |-  ( ( ( ph /\ -. B = C ) /\ -. C < B ) -> ( ph /\ B < C ) )
95 41 adantr 
 |-  ( ( ph /\ B < C ) -> P e. NN )
96 1zzd 
 |-  ( ( ph /\ B < C ) -> 1 e. ZZ )
97 41 nnzd 
 |-  ( ph -> P e. ZZ )
98 97 adantr 
 |-  ( ( ph /\ B < C ) -> P e. ZZ )
99 98 96 zsubcld 
 |-  ( ( ph /\ B < C ) -> ( P - 1 ) e. ZZ )
100 16 adantr 
 |-  ( ( ph /\ B < C ) -> C e. ZZ )
101 18 adantr 
 |-  ( ( ph /\ B < C ) -> B e. ZZ )
102 100 101 zsubcld 
 |-  ( ( ph /\ B < C ) -> ( C - B ) e. ZZ )
103 49 a1i 
 |-  ( ( ph /\ B < C ) -> 1 = ( 0 + 1 ) )
104 55 52 posdifd 
 |-  ( ph -> ( B < C <-> 0 < ( C - B ) ) )
105 104 biimpd 
 |-  ( ph -> ( B < C -> 0 < ( C - B ) ) )
106 105 imp 
 |-  ( ( ph /\ B < C ) -> 0 < ( C - B ) )
107 0zd 
 |-  ( ( ph /\ B < C ) -> 0 e. ZZ )
108 107 102 zltp1led 
 |-  ( ( ph /\ B < C ) -> ( 0 < ( C - B ) <-> ( 0 + 1 ) <_ ( C - B ) ) )
109 106 108 mpbid 
 |-  ( ( ph /\ B < C ) -> ( 0 + 1 ) <_ ( C - B ) )
110 103 109 eqbrtrd 
 |-  ( ( ph /\ B < C ) -> 1 <_ ( C - B ) )
111 102 zred 
 |-  ( ( ph /\ B < C ) -> ( C - B ) e. RR )
112 52 adantr 
 |-  ( ( ph /\ B < C ) -> C e. RR )
113 73 adantr 
 |-  ( ( ph /\ B < C ) -> P e. RR )
114 9 adantr 
 |-  ( ( ph /\ B < C ) -> B e. ( 0 ... A ) )
115 elfzle1 
 |-  ( B e. ( 0 ... A ) -> 0 <_ B )
116 114 115 syl 
 |-  ( ( ph /\ B < C ) -> 0 <_ B )
117 55 adantr 
 |-  ( ( ph /\ B < C ) -> B e. RR )
118 112 117 subge02d 
 |-  ( ( ph /\ B < C ) -> ( 0 <_ B <-> ( C - B ) <_ C ) )
119 116 118 mpbid 
 |-  ( ( ph /\ B < C ) -> ( C - B ) <_ C )
120 72 adantr 
 |-  ( ( ph /\ B < C ) -> A e. RR )
121 elfzle2 
 |-  ( C e. ( 0 ... A ) -> C <_ A )
122 10 121 syl 
 |-  ( ph -> C <_ A )
123 122 adantr 
 |-  ( ( ph /\ B < C ) -> C <_ A )
124 5 adantr 
 |-  ( ( ph /\ B < C ) -> A < P )
125 112 120 113 123 124 lelttrd 
 |-  ( ( ph /\ B < C ) -> C < P )
126 111 112 113 119 125 lelttrd 
 |-  ( ( ph /\ B < C ) -> ( C - B ) < P )
127 102 98 zltlem1d 
 |-  ( ( ph /\ B < C ) -> ( ( C - B ) < P <-> ( C - B ) <_ ( P - 1 ) ) )
128 126 127 mpbid 
 |-  ( ( ph /\ B < C ) -> ( C - B ) <_ ( P - 1 ) )
129 96 99 102 110 128 elfzd 
 |-  ( ( ph /\ B < C ) -> ( C - B ) e. ( 1 ... ( P - 1 ) ) )
130 fzm1ndvds 
 |-  ( ( P e. NN /\ ( C - B ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( C - B ) )
131 95 129 130 syl2anc 
 |-  ( ( ph /\ B < C ) -> -. P || ( C - B ) )
132 dvdsnegb 
 |-  ( ( P e. ZZ /\ ( B - C ) e. ZZ ) -> ( P || ( B - C ) <-> P || -u ( B - C ) ) )
133 97 47 132 syl2anc 
 |-  ( ph -> ( P || ( B - C ) <-> P || -u ( B - C ) ) )
134 19 17 negsubdi2d 
 |-  ( ph -> -u ( B - C ) = ( C - B ) )
135 134 breq2d 
 |-  ( ph -> ( P || -u ( B - C ) <-> P || ( C - B ) ) )
136 133 135 bitrd 
 |-  ( ph -> ( P || ( B - C ) <-> P || ( C - B ) ) )
137 136 adantr 
 |-  ( ( ph /\ B < C ) -> ( P || ( B - C ) <-> P || ( C - B ) ) )
138 131 137 mtbird 
 |-  ( ( ph /\ B < C ) -> -. P || ( B - C ) )
139 94 138 syl 
 |-  ( ( ( ph /\ -. B = C ) /\ -. C < B ) -> -. P || ( B - C ) )
140 84 139 pm2.61dan 
 |-  ( ( ph /\ -. B = C ) -> -. P || ( B - C ) )
141 140 ex 
 |-  ( ph -> ( -. B = C -> -. P || ( B - C ) ) )
142 141 con4d 
 |-  ( ph -> ( P || ( B - C ) -> B = C ) )
143 40 142 impbid 
 |-  ( ph -> ( B = C <-> P || ( B - C ) ) )
144 1 fldcrngd 
 |-  ( ph -> K e. CRing )
145 crngring 
 |-  ( K e. CRing -> K e. Ring )
146 144 145 syl 
 |-  ( ph -> K e. Ring )
147 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
148 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
149 3 147 148 chrdvds 
 |-  ( ( K e. Ring /\ ( B - C ) e. ZZ ) -> ( P || ( B - C ) <-> ( ( ZRHom ` K ) ` ( B - C ) ) = ( 0g ` K ) ) )
150 146 47 149 syl2anc 
 |-  ( ph -> ( P || ( B - C ) <-> ( ( ZRHom ` K ) ` ( B - C ) ) = ( 0g ` K ) ) )
151 143 150 bitr2d 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( B - C ) ) = ( 0g ` K ) <-> B = C ) )
152 26 151 bitrd 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( 0g ` K ) <-> B = C ) )
153 152 bicomd 
 |-  ( ph -> ( B = C <-> ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( 0g ` K ) ) )
154 147 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
155 rhmghm 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
156 154 155 syl 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
157 146 156 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
158 0zd 
 |-  ( ph -> 0 e. ZZ )
159 158 16 zsubcld 
 |-  ( ph -> ( 0 - C ) e. ZZ )
160 zringbas 
 |-  ZZ = ( Base ` ZZring )
161 159 160 eleqtrdi 
 |-  ( ph -> ( 0 - C ) e. ( Base ` ZZring ) )
162 18 160 eleqtrdi 
 |-  ( ph -> B e. ( Base ` ZZring ) )
163 eqid 
 |-  ( Base ` ZZring ) = ( Base ` ZZring )
164 eqid 
 |-  ( +g ` ZZring ) = ( +g ` ZZring )
165 eqid 
 |-  ( +g ` K ) = ( +g ` K )
166 163 164 165 ghmlin 
 |-  ( ( ( ZRHom ` K ) e. ( ZZring GrpHom K ) /\ ( 0 - C ) e. ( Base ` ZZring ) /\ B e. ( Base ` ZZring ) ) -> ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) )
167 157 161 162 166 syl3anc 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) )
168 167 eqeq1d 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( ( 0 - C ) ( +g ` ZZring ) B ) ) = ( 0g ` K ) <-> ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) = ( 0g ` K ) ) )
169 153 168 bitrd 
 |-  ( ph -> ( B = C <-> ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) = ( 0g ` K ) ) )
170 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
171 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
172 eqid 
 |-  ( Base ` K ) = ( Base ` K )
173 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
174 160 172 ghmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring GrpHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
175 157 174 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
176 175 159 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( 0 - C ) ) e. ( Base ` K ) )
177 170 6 172 171 173 144 176 evl1vard 
 |-  ( ph -> ( X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` X ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( ( ZRHom ` K ) ` ( 0 - C ) ) ) )
178 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
179 175 18 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` B ) e. ( Base ` K ) )
180 170 171 172 178 173 144 179 176 evl1scad 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( ( ZRHom ` K ) ` B ) ) )
181 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
182 170 171 172 173 144 176 177 180 181 165 evl1addd 
 |-  ( ph -> ( ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) ) )
183 182 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) )
184 183 eqcomd 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) = ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) )
185 184 eqeq1d 
 |-  ( ph -> ( ( ( ( ZRHom ` K ) ` ( 0 - C ) ) ( +g ` K ) ( ( ZRHom ` K ) ` B ) ) = ( 0g ` K ) <-> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( 0g ` K ) ) )
186 169 185 bitrd 
 |-  ( ph -> ( B = C <-> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` B ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - C ) ) ) = ( 0g ` K ) ) )