Metamath Proof Explorer

Theorem aks6d1c5lem2

Description: Lemma for Claim 5, contradiction of different evaluations that map to the same. (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 ) ) ) ) ) ) )
aks6d1c5p2.1 
|- ( ph -> Y e. ( NN0 ^m ( 0 ... A ) ) )
aks6d1c5p2.2 
|- ( ph -> Z e. ( NN0 ^m ( 0 ... A ) ) )
aks6d1c5p2.3 
|- ( ph -> ( G ` Y ) = ( G ` Z ) )
aks6d1c5p2.4 
|- ( ph -> W e. ( 0 ... A ) )
aks6d1c5p2.5 
|- ( ph -> ( Y ` W ) < ( Z ` W ) )
Assertion aks6d1c5lem2 
|- ( ph -> ( 0g ` K ) =/= ( 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 aks6d1c5p2.1 
 |-  ( ph -> Y e. ( NN0 ^m ( 0 ... A ) ) )
10 aks6d1c5p2.2 
 |-  ( ph -> Z e. ( NN0 ^m ( 0 ... A ) ) )
11 aks6d1c5p2.3 
 |-  ( ph -> ( G ` Y ) = ( G ` Z ) )
12 aks6d1c5p2.4 
 |-  ( ph -> W e. ( 0 ... A ) )
13 aks6d1c5p2.5 
 |-  ( ph -> ( Y ` W ) < ( Z ` W ) )
14 eqid 
 |-  ( eval1 ` K ) = ( eval1 ` K )
15 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
18 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
19 18 simprbi 
 |-  ( K e. Field -> K e. CRing )
20 1 19 syl 
 |-  ( ph -> K e. CRing )
21 20 crngringd 
 |-  ( ph -> K e. Ring )
22 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
23 22 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
24 21 23 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
25 zringbas 
 |-  ZZ = ( Base ` ZZring )
26 25 16 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
27 24 26 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
28 0zd 
 |-  ( ph -> 0 e. ZZ )
29 12 elfzelzd 
 |-  ( ph -> W e. ZZ )
30 28 29 zsubcld 
 |-  ( ph -> ( 0 - W ) e. ZZ )
31 27 30 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( 0 - W ) ) e. ( Base ` K ) )
32 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
33 32 17 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
34 15 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
35 20 34 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
36 32 crngmgp 
 |-  ( ( Poly1 ` K ) e. CRing -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
37 35 36 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
38 37 cmnmndd 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
39 nn0ex 
 |-  NN0 e. _V
40 39 a1i 
 |-  ( ph -> NN0 e. _V )
41 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
42 elmapg 
 |-  ( ( NN0 e. _V /\ ( 0 ... A ) e. _V ) -> ( Y e. ( NN0 ^m ( 0 ... A ) ) <-> Y : ( 0 ... A ) --> NN0 ) )
43 40 41 42 syl2anc 
 |-  ( ph -> ( Y e. ( NN0 ^m ( 0 ... A ) ) <-> Y : ( 0 ... A ) --> NN0 ) )
44 9 43 mpbid 
 |-  ( ph -> Y : ( 0 ... A ) --> NN0 )
45 44 12 ffvelcdmd 
 |-  ( ph -> ( Y ` W ) e. NN0 )
46 45 nn0zd 
 |-  ( ph -> ( Y ` W ) e. ZZ )
47 46 46 zsubcld 
 |-  ( ph -> ( ( Y ` W ) - ( Y ` W ) ) e. ZZ )
48 0red 
 |-  ( ph -> 0 e. RR )
49 48 leidd 
 |-  ( ph -> 0 <_ 0 )
50 45 nn0red 
 |-  ( ph -> ( Y ` W ) e. RR )
51 50 recnd 
 |-  ( ph -> ( Y ` W ) e. CC )
52 51 subidd 
 |-  ( ph -> ( ( Y ` W ) - ( Y ` W ) ) = 0 )
53 52 eqcomd 
 |-  ( ph -> 0 = ( ( Y ` W ) - ( Y ` W ) ) )
54 49 53 breqtrd 
 |-  ( ph -> 0 <_ ( ( Y ` W ) - ( Y ` W ) ) )
55 47 54 jca 
 |-  ( ph -> ( ( ( Y ` W ) - ( Y ` W ) ) e. ZZ /\ 0 <_ ( ( Y ` W ) - ( Y ` W ) ) ) )
56 elnn0z 
 |-  ( ( ( Y ` W ) - ( Y ` W ) ) e. NN0 <-> ( ( ( Y ` W ) - ( Y ` W ) ) e. ZZ /\ 0 <_ ( ( Y ` W ) - ( Y ` W ) ) ) )
57 55 56 sylibr 
 |-  ( ph -> ( ( Y ` W ) - ( Y ` W ) ) e. NN0 )
58 14 6 16 15 17 20 31 evl1vard 
 |-  ( ph -> ( X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` X ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
59 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
60 27 29 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` W ) e. ( Base ` K ) )
61 14 15 16 59 17 20 60 31 evl1scad 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ZRHom ` K ) ` W ) ) )
62 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
63 eqid 
 |-  ( +g ` K ) = ( +g ` K )
64 14 15 16 17 20 31 58 61 62 63 evl1addd 
 |-  ( ph -> ( ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) ) )
65 64 simpld 
 |-  ( ph -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
66 33 7 38 57 65 mulgnn0cld 
 |-  ( ph -> ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
67 52 oveq1d 
 |-  ( ph -> ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( 0 .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) )
68 eqid 
 |-  ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) )
69 33 68 7 mulg0 
 |-  ( ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) -> ( 0 .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) )
70 65 69 syl 
 |-  ( ph -> ( 0 .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) )
71 67 70 eqtrd 
 |-  ( ph -> ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) )
72 71 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( eval1 ` K ) ` ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) ) )
73 72 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
74 eqid 
 |-  ( 1r ` ( Poly1 ` K ) ) = ( 1r ` ( Poly1 ` K ) )
75 32 74 ringidval 
 |-  ( 1r ` ( Poly1 ` K ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) )
76 75 eqcomi 
 |-  ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( 1r ` ( Poly1 ` K ) )
77 76 a1i 
 |-  ( ph -> ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( 1r ` ( Poly1 ` K ) ) )
78 77 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) ) = ( ( eval1 ` K ) ` ( 1r ` ( Poly1 ` K ) ) ) )
79 78 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( 1r ` ( Poly1 ` K ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
80 15 6 32 7 ply1idvr1 
 |-  ( K e. Ring -> ( 0 .^ X ) = ( 1r ` ( Poly1 ` K ) ) )
81 80 eqcomd 
 |-  ( K e. Ring -> ( 1r ` ( Poly1 ` K ) ) = ( 0 .^ X ) )
82 21 81 syl 
 |-  ( ph -> ( 1r ` ( Poly1 ` K ) ) = ( 0 .^ X ) )
83 82 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( 1r ` ( Poly1 ` K ) ) ) = ( ( eval1 ` K ) ` ( 0 .^ X ) ) )
84 83 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 1r ` ( Poly1 ` K ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( 0 .^ X ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
85 eqid 
 |-  ( .g ` ( mulGrp ` K ) ) = ( .g ` ( mulGrp ` K ) )
86 53 57 eqeltrd 
 |-  ( ph -> 0 e. NN0 )
87 14 15 16 17 20 31 58 7 85 86 evl1expd 
 |-  ( ph -> ( ( 0 .^ X ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( 0 .^ X ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0 ( .g ` ( mulGrp ` K ) ) ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) )
88 87 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 0 .^ X ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0 ( .g ` ( mulGrp ` K ) ) ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
89 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
90 89 16 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
91 90 a1i 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( mulGrp ` K ) ) )
92 31 91 eleqtrd 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( 0 - W ) ) e. ( Base ` ( mulGrp ` K ) ) )
93 eqid 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` ( mulGrp ` K ) )
94 eqid 
 |-  ( 0g ` ( mulGrp ` K ) ) = ( 0g ` ( mulGrp ` K ) )
95 93 94 85 mulg0 
 |-  ( ( ( ZRHom ` K ) ` ( 0 - W ) ) e. ( Base ` ( mulGrp ` K ) ) -> ( 0 ( .g ` ( mulGrp ` K ) ) ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` ( mulGrp ` K ) ) )
96 92 95 syl 
 |-  ( ph -> ( 0 ( .g ` ( mulGrp ` K ) ) ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` ( mulGrp ` K ) ) )
97 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
98 89 97 ringidval 
 |-  ( 1r ` K ) = ( 0g ` ( mulGrp ` K ) )
99 98 eqcomi 
 |-  ( 0g ` ( mulGrp ` K ) ) = ( 1r ` K )
100 99 a1i 
 |-  ( ph -> ( 0g ` ( mulGrp ` K ) ) = ( 1r ` K ) )
101 96 100 eqtrd 
 |-  ( ph -> ( 0 ( .g ` ( mulGrp ` K ) ) ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) )
102 88 101 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 0 .^ X ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) )
103 84 102 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 1r ` ( Poly1 ` K ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) )
104 79 103 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( 0g ` ( mulGrp ` ( Poly1 ` K ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) )
105 73 104 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) )
106 66 105 jca 
 |-  ( ph -> ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 1r ` K ) ) )
107 fzfid 
 |-  ( ph -> ( 0 ... A ) e. Fin )
108 diffi 
 |-  ( ( 0 ... A ) e. Fin -> ( ( 0 ... A ) \ { W } ) e. Fin )
109 107 108 syl 
 |-  ( ph -> ( ( 0 ... A ) \ { W } ) e. Fin )
110 38 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
111 44 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> Y : ( 0 ... A ) --> NN0 )
112 eldifi 
 |-  ( i e. ( ( 0 ... A ) \ { W } ) -> i e. ( 0 ... A ) )
113 112 adantl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> i e. ( 0 ... A ) )
114 111 113 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Y ` i ) e. NN0 )
115 35 crngringd 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
116 ringcmn 
 |-  ( ( Poly1 ` K ) e. Ring -> ( Poly1 ` K ) e. CMnd )
117 115 116 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CMnd )
118 cmnmnd 
 |-  ( ( Poly1 ` K ) e. CMnd -> ( Poly1 ` K ) e. Mnd )
119 117 118 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Mnd )
120 119 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Poly1 ` K ) e. Mnd )
121 58 simpld 
 |-  ( ph -> X e. ( Base ` ( Poly1 ` K ) ) )
122 121 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> X e. ( Base ` ( Poly1 ` K ) ) )
123 21 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> K e. Ring )
124 123 23 26 3syl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
125 113 elfzelzd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> i e. ZZ )
126 124 125 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
127 15 59 16 17 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
128 123 126 127 syl2anc 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
129 17 62 mndcl 
 |-  ( ( ( Poly1 ` K ) e. Mnd /\ X e. ( Base ` ( Poly1 ` K ) ) /\ ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
130 120 122 128 129 syl3anc 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
131 33 7 110 114 130 mulgnn0cld 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
132 131 ralrimiva 
 |-  ( ph -> A. i e. ( ( 0 ... A ) \ { W } ) ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
133 33 37 109 132 gsummptcl 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
134 132 r19.21bi 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
135 134 ralrimiva 
 |-  ( ph -> A. i e. ( ( 0 ... A ) \ { W } ) ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
136 14 15 32 16 17 89 20 31 135 109 evl1gprodd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) )
137 133 136 jca 
 |-  ( ph -> ( ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) ) )
138 eqid 
 |-  ( .r ` ( Poly1 ` K ) ) = ( .r ` ( Poly1 ` K ) )
139 32 138 mgpplusg 
 |-  ( .r ` ( Poly1 ` K ) ) = ( +g ` ( mulGrp ` ( Poly1 ` K ) ) )
140 139 eqcomi 
 |-  ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .r ` ( Poly1 ` K ) )
141 eqid 
 |-  ( .r ` K ) = ( .r ` K )
142 14 15 16 17 20 31 106 137 140 141 evl1muld 
 |-  ( ph -> ( ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( 1r ` K ) ( .r ` K ) ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) ) ) )
143 142 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( 1r ` K ) ( .r ` K ) ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) ) )
144 fldidom 
 |-  ( K e. Field -> K e. IDomn )
145 1 144 syl 
 |-  ( ph -> K e. IDomn )
146 isidom 
 |-  ( K e. IDomn <-> ( K e. CRing /\ K e. Domn ) )
147 145 146 sylib 
 |-  ( ph -> ( K e. CRing /\ K e. Domn ) )
148 147 simprd 
 |-  ( ph -> K e. Domn )
149 98 a1i 
 |-  ( ph -> ( 1r ` K ) = ( 0g ` ( mulGrp ` K ) ) )
150 89 ringmgp 
 |-  ( K e. Ring -> ( mulGrp ` K ) e. Mnd )
151 21 150 syl 
 |-  ( ph -> ( mulGrp ` K ) e. Mnd )
152 90 94 mndidcl 
 |-  ( ( mulGrp ` K ) e. Mnd -> ( 0g ` ( mulGrp ` K ) ) e. ( Base ` K ) )
153 151 152 syl 
 |-  ( ph -> ( 0g ` ( mulGrp ` K ) ) e. ( Base ` K ) )
154 149 153 eqeltrd 
 |-  ( ph -> ( 1r ` K ) e. ( Base ` K ) )
155 1 flddrngd 
 |-  ( ph -> K e. DivRing )
156 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
157 156 97 drngunz 
 |-  ( K e. DivRing -> ( 1r ` K ) =/= ( 0g ` K ) )
158 155 157 syl 
 |-  ( ph -> ( 1r ` K ) =/= ( 0g ` K ) )
159 154 158 jca 
 |-  ( ph -> ( ( 1r ` K ) e. ( Base ` K ) /\ ( 1r ` K ) =/= ( 0g ` K ) ) )
160 89 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
161 20 160 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
162 20 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> K e. CRing )
163 31 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ZRHom ` K ) ` ( 0 - W ) ) e. ( Base ` K ) )
164 14 15 16 17 162 163 131 fveval1fvcl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) e. ( Base ` K ) )
165 164 ralrimiva 
 |-  ( ph -> A. i e. ( ( 0 ... A ) \ { W } ) ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) e. ( Base ` K ) )
166 90 161 109 165 gsummptcl 
 |-  ( ph -> ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) e. ( Base ` K ) )
167 33 a1i 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
168 130 167 eleqtrd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
169 33 eqcomi 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) )
170 169 a1i 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) ) )
171 168 170 eleqtrd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
172 eqidd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
173 171 172 jca 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) )
174 14 15 16 17 162 163 173 7 85 114 evl1expd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( Y ` i ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) )
175 174 simprd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( Y ` i ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) )
176 145 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> K e. IDomn )
177 14 15 16 17 162 163 171 fveval1fvcl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) e. ( Base ` K ) )
178 eldifsni 
 |-  ( i e. ( ( 0 ... A ) \ { W } ) -> i =/= W )
179 178 adantl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> i =/= W )
180 1 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> K e. Field )
181 2 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> P e. Prime )
182 4 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> A e. NN0 )
183 5 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> A < P )
184 12 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> W e. ( 0 ... A ) )
185 180 181 3 182 183 6 7 8 113 184 aks6d1c5lem1 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( i = W <-> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` K ) ) )
186 185 necon3bid 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( i =/= W <-> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) =/= ( 0g ` K ) ) )
187 179 186 mpbid 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) =/= ( 0g ` K ) )
188 176 177 187 114 85 idomnnzpownz 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Y ` i ) ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) =/= ( 0g ` K ) )
189 175 188 eqnetrd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) =/= ( 0g ` K ) )
190 89 145 109 164 189 idomnnzgmulnz 
 |-  ( ph -> ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) =/= ( 0g ` K ) )
191 166 190 jca 
 |-  ( ph -> ( ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) e. ( Base ` K ) /\ ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) =/= ( 0g ` K ) ) )
192 16 141 156 domnmuln0 
 |-  ( ( K e. Domn /\ ( ( 1r ` K ) e. ( Base ` K ) /\ ( 1r ` K ) =/= ( 0g ` K ) ) /\ ( ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) e. ( Base ` K ) /\ ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) =/= ( 0g ` K ) ) ) -> ( ( 1r ` K ) ( .r ` K ) ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) ) =/= ( 0g ` K ) )
193 148 159 191 192 syl3anc 
 |-  ( ph -> ( ( 1r ` K ) ( .r ` K ) ( ( mulGrp ` K ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( ( eval1 ` K ) ` ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) ) =/= ( 0g ` K ) )
194 143 193 eqnetrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) =/= ( 0g ` K ) )
195 194 necomd 
 |-  ( ph -> ( 0g ` K ) =/= ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
196 50 leidd 
 |-  ( ph -> ( Y ` W ) <_ ( Y ` W ) )
197 eqid 
 |-  ( quot1p ` K ) = ( quot1p ` K )
198 1 2 3 4 5 6 7 8 9 12 45 196 197 59 32 aks6d1c5lem3 
 |-  ( ph -> ( ( G ` Y ) ( quot1p ` K ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
199 198 eqcomd 
 |-  ( ph -> ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = ( ( G ` Y ) ( quot1p ` K ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
200 11 oveq1d 
 |-  ( ph -> ( ( G ` Y ) ( quot1p ` K ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( G ` Z ) ( quot1p ` K ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
201 elmapg 
 |-  ( ( NN0 e. _V /\ ( 0 ... A ) e. _V ) -> ( Z e. ( NN0 ^m ( 0 ... A ) ) <-> Z : ( 0 ... A ) --> NN0 ) )
202 40 41 201 syl2anc 
 |-  ( ph -> ( Z e. ( NN0 ^m ( 0 ... A ) ) <-> Z : ( 0 ... A ) --> NN0 ) )
203 10 202 mpbid 
 |-  ( ph -> Z : ( 0 ... A ) --> NN0 )
204 203 12 ffvelcdmd 
 |-  ( ph -> ( Z ` W ) e. NN0 )
205 204 nn0red 
 |-  ( ph -> ( Z ` W ) e. RR )
206 50 205 13 ltled 
 |-  ( ph -> ( Y ` W ) <_ ( Z ` W ) )
207 1 2 3 4 5 6 7 8 10 12 45 206 197 59 32 aks6d1c5lem3 
 |-  ( ph -> ( ( G ` Z ) ( quot1p ` K ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
208 199 200 207 3eqtrd 
 |-  ( ph -> ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
209 208 fveq2d 
 |-  ( ph -> ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) = ( ( eval1 ` K ) ` ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) )
210 209 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
211 204 nn0zd 
 |-  ( ph -> ( Z ` W ) e. ZZ )
212 211 46 zsubcld 
 |-  ( ph -> ( ( Z ` W ) - ( Y ` W ) ) e. ZZ )
213 205 50 resubcld 
 |-  ( ph -> ( ( Z ` W ) - ( Y ` W ) ) e. RR )
214 50 205 posdifd 
 |-  ( ph -> ( ( Y ` W ) < ( Z ` W ) <-> 0 < ( ( Z ` W ) - ( Y ` W ) ) ) )
215 13 214 mpbid 
 |-  ( ph -> 0 < ( ( Z ` W ) - ( Y ` W ) ) )
216 48 213 215 ltled 
 |-  ( ph -> 0 <_ ( ( Z ` W ) - ( Y ` W ) ) )
217 212 216 jca 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) e. ZZ /\ 0 <_ ( ( Z ` W ) - ( Y ` W ) ) ) )
218 elnn0z 
 |-  ( ( ( Z ` W ) - ( Y ` W ) ) e. NN0 <-> ( ( ( Z ` W ) - ( Y ` W ) ) e. ZZ /\ 0 <_ ( ( Z ` W ) - ( Y ` W ) ) ) )
219 217 218 sylibr 
 |-  ( ph -> ( ( Z ` W ) - ( Y ` W ) ) e. NN0 )
220 14 15 16 17 20 31 64 7 85 219 evl1expd 
 |-  ( ph -> ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) ) ) )
221 220 simpld 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
222 220 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) ) )
223 rhmghm 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
224 24 223 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
225 30 25 eleqtrdi 
 |-  ( ph -> ( 0 - W ) e. ( Base ` ZZring ) )
226 29 25 eleqtrdi 
 |-  ( ph -> W e. ( Base ` ZZring ) )
227 eqid 
 |-  ( Base ` ZZring ) = ( Base ` ZZring )
228 eqid 
 |-  ( +g ` ZZring ) = ( +g ` ZZring )
229 227 228 63 ghmlin 
 |-  ( ( ( ZRHom ` K ) e. ( ZZring GrpHom K ) /\ ( 0 - W ) e. ( Base ` ZZring ) /\ W e. ( Base ` ZZring ) ) -> ( ( ZRHom ` K ) ` ( ( 0 - W ) ( +g ` ZZring ) W ) ) = ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) )
230 224 225 226 229 syl3anc 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - W ) ( +g ` ZZring ) W ) ) = ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) )
231 zringplusg 
 |-  + = ( +g ` ZZring )
232 231 eqcomi 
 |-  ( +g ` ZZring ) = +
233 232 a1i 
 |-  ( ph -> ( +g ` ZZring ) = + )
234 233 oveqd 
 |-  ( ph -> ( ( 0 - W ) ( +g ` ZZring ) W ) = ( ( 0 - W ) + W ) )
235 234 fveq2d 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - W ) ( +g ` ZZring ) W ) ) = ( ( ZRHom ` K ) ` ( ( 0 - W ) + W ) ) )
236 0cnd 
 |-  ( ph -> 0 e. CC )
237 29 zcnd 
 |-  ( ph -> W e. CC )
238 236 237 npcand 
 |-  ( ph -> ( ( 0 - W ) + W ) = 0 )
239 238 fveq2d 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - W ) + W ) ) = ( ( ZRHom ` K ) ` 0 ) )
240 235 239 eqtrd 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - W ) ( +g ` ZZring ) W ) ) = ( ( ZRHom ` K ) ` 0 ) )
241 22 156 zrh0 
 |-  ( K e. Ring -> ( ( ZRHom ` K ) ` 0 ) = ( 0g ` K ) )
242 21 241 syl 
 |-  ( ph -> ( ( ZRHom ` K ) ` 0 ) = ( 0g ` K ) )
243 240 242 eqtrd 
 |-  ( ph -> ( ( ZRHom ` K ) ` ( ( 0 - W ) ( +g ` ZZring ) W ) ) = ( 0g ` K ) )
244 230 243 eqtr3d 
 |-  ( ph -> ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) = ( 0g ` K ) )
245 244 oveq2d 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) ) = ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( 0g ` K ) ) )
246 219 nn0zd 
 |-  ( ph -> ( ( Z ` W ) - ( Y ` W ) ) e. ZZ )
247 246 215 jca 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) e. ZZ /\ 0 < ( ( Z ` W ) - ( Y ` W ) ) ) )
248 elnnz 
 |-  ( ( ( Z ` W ) - ( Y ` W ) ) e. NN <-> ( ( ( Z ` W ) - ( Y ` W ) ) e. ZZ /\ 0 < ( ( Z ` W ) - ( Y ` W ) ) ) )
249 247 248 sylibr 
 |-  ( ph -> ( ( Z ` W ) - ( Y ` W ) ) e. NN )
250 21 249 85 ringexp0nn 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( 0g ` K ) ) = ( 0g ` K ) )
251 245 250 eqtrd 
 |-  ( ph -> ( ( ( Z ` W ) - ( Y ` W ) ) ( .g ` ( mulGrp ` K ) ) ( ( ( ZRHom ` K ) ` ( 0 - W ) ) ( +g ` K ) ( ( ZRHom ` K ) ` W ) ) ) = ( 0g ` K ) )
252 222 251 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` K ) )
253 221 252 jca 
 |-  ( ph -> ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` K ) ) )
254 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
255 203 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> Z : ( 0 ... A ) --> NN0 )
256 255 113 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Z ` i ) e. NN0 )
257 254 7 110 256 168 mulgnn0cld 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
258 257 170 eleqtrd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
259 258 ralrimiva 
 |-  ( ph -> A. i e. ( ( 0 ... A ) \ { W } ) ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
260 33 37 109 259 gsummptcl 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
261 eqidd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) )
262 260 261 jca 
 |-  ( ph -> ( ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) )
263 14 15 16 17 20 31 253 262 140 141 evl1muld 
 |-  ( ph -> ( ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( ( eval1 ` K ) ` ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( 0g ` K ) ( .r ` K ) ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) ) )
264 263 simprd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( ( 0g ` K ) ( .r ` K ) ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) )
265 14 15 16 17 20 31 260 fveval1fvcl 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) e. ( Base ` K ) )
266 16 141 156 21 265 ringlzd 
 |-  ( ph -> ( ( 0g ` K ) ( .r ` K ) ( ( ( eval1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) ) = ( 0g ` K ) )
267 264 266 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Z ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Z ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` K ) )
268 210 267 eqtrd 
 |-  ( ph -> ( ( ( eval1 ` K ) ` ( ( ( ( Y ` W ) - ( Y ` W ) ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) ` ( ( ZRHom ` K ) ` ( 0 - W ) ) ) = ( 0g ` K ) )
269 195 268 neeqtrd 
 |-  ( ph -> ( 0g ` K ) =/= ( 0g ` K ) )