Metamath Proof Explorer

Theorem aks6d1c5lem3

Description: Lemma for Claim 5, polynomial division with a linear power. (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 ) ) ) ) ) ) )
aks6d1c5p3.1 
|- ( ph -> Y e. ( NN0 ^m ( 0 ... A ) ) )
aks6d1c5p3.2 
|- ( ph -> W e. ( 0 ... A ) )
aks6d1c5p3.3 
|- ( ph -> C e. NN0 )
aks6d1c5p3.4 
|- ( ph -> C <_ ( Y ` W ) )
aks6d1c5p3.5 
|- Q = ( quot1p ` K )
aks6d1c5p3.6 
|- S = ( algSc ` ( Poly1 ` K ) )
aks6d1c5p3.7 
|- M = ( mulGrp ` ( Poly1 ` K ) )
Assertion aks6d1c5lem3 
|- ( ph -> ( ( G ` Y ) Q ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )

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 aks6d1c5p3.1 
 |-  ( ph -> Y e. ( NN0 ^m ( 0 ... A ) ) )
10 aks6d1c5p3.2 
 |-  ( ph -> W e. ( 0 ... A ) )
11 aks6d1c5p3.3 
 |-  ( ph -> C e. NN0 )
12 aks6d1c5p3.4 
 |-  ( ph -> C <_ ( Y ` W ) )
13 aks6d1c5p3.5 
 |-  Q = ( quot1p ` K )
14 aks6d1c5p3.6 
 |-  S = ( algSc ` ( Poly1 ` K ) )
15 aks6d1c5p3.7 
 |-  M = ( mulGrp ` ( Poly1 ` K ) )
16 1 fldcrngd 
 |-  ( ph -> K e. CRing )
17 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
18 17 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
19 16 18 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
20 crngring 
 |-  ( ( Poly1 ` K ) e. CRing -> ( Poly1 ` K ) e. Ring )
21 19 20 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
22 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
23 22 ringmgp 
 |-  ( ( Poly1 ` K ) e. Ring -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
24 21 23 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
25 15 24 eqeltrid 
 |-  ( ph -> M e. Mnd )
26 15 fveq2i 
 |-  ( Base ` M ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
27 nn0ex 
 |-  NN0 e. _V
28 27 a1i 
 |-  ( ph -> NN0 e. _V )
29 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
30 elmapg 
 |-  ( ( NN0 e. _V /\ ( 0 ... A ) e. _V ) -> ( Y e. ( NN0 ^m ( 0 ... A ) ) <-> Y : ( 0 ... A ) --> NN0 ) )
31 28 29 30 syl2anc 
 |-  ( ph -> ( Y e. ( NN0 ^m ( 0 ... A ) ) <-> Y : ( 0 ... A ) --> NN0 ) )
32 9 31 mpbid 
 |-  ( ph -> Y : ( 0 ... A ) --> NN0 )
33 32 10 ffvelcdmd 
 |-  ( ph -> ( Y ` W ) e. NN0 )
34 33 nn0zd 
 |-  ( ph -> ( Y ` W ) e. ZZ )
35 11 nn0zd 
 |-  ( ph -> C e. ZZ )
36 34 35 zsubcld 
 |-  ( ph -> ( ( Y ` W ) - C ) e. ZZ )
37 33 nn0red 
 |-  ( ph -> ( Y ` W ) e. RR )
38 11 nn0red 
 |-  ( ph -> C e. RR )
39 37 38 subge0d 
 |-  ( ph -> ( 0 <_ ( ( Y ` W ) - C ) <-> C <_ ( Y ` W ) ) )
40 12 39 mpbird 
 |-  ( ph -> 0 <_ ( ( Y ` W ) - C ) )
41 36 40 jca 
 |-  ( ph -> ( ( ( Y ` W ) - C ) e. ZZ /\ 0 <_ ( ( Y ` W ) - C ) ) )
42 elnn0z 
 |-  ( ( ( Y ` W ) - C ) e. NN0 <-> ( ( ( Y ` W ) - C ) e. ZZ /\ 0 <_ ( ( Y ` W ) - C ) ) )
43 41 42 sylibr 
 |-  ( ph -> ( ( Y ` W ) - C ) e. NN0 )
44 21 ringcmnd 
 |-  ( ph -> ( Poly1 ` K ) e. CMnd )
45 cmnmnd 
 |-  ( ( Poly1 ` K ) e. CMnd -> ( Poly1 ` K ) e. Mnd )
46 44 45 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Mnd )
47 crngring 
 |-  ( K e. CRing -> K e. Ring )
48 16 47 syl 
 |-  ( ph -> K e. Ring )
49 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
50 6 17 49 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` ( Poly1 ` K ) ) )
51 48 50 syl 
 |-  ( ph -> X e. ( Base ` ( Poly1 ` K ) ) )
52 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
53 52 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
54 48 53 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
55 zringbas 
 |-  ZZ = ( Base ` ZZring )
56 eqid 
 |-  ( Base ` K ) = ( Base ` K )
57 55 56 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
58 54 57 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
59 10 elfzelzd 
 |-  ( ph -> W e. ZZ )
60 58 59 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` W ) e. ( Base ` K ) )
61 17 14 56 49 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` W ) e. ( Base ` K ) ) -> ( S ` ( ( ZRHom ` K ) ` W ) ) e. ( Base ` ( Poly1 ` K ) ) )
62 48 60 61 syl2anc 
 |-  ( ph -> ( S ` ( ( ZRHom ` K ) ` W ) ) e. ( Base ` ( Poly1 ` K ) ) )
63 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
64 49 63 mndcl 
 |-  ( ( ( Poly1 ` K ) e. Mnd /\ X e. ( Base ` ( Poly1 ` K ) ) /\ ( S ` ( ( ZRHom ` K ) ` W ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
65 46 51 62 64 syl3anc 
 |-  ( ph -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
66 22 49 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
67 66 eqcomi 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) )
68 26 67 eqtri 
 |-  ( Base ` M ) = ( Base ` ( Poly1 ` K ) )
69 65 68 eleqtrrdi 
 |-  ( ph -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` M ) )
70 26 7 24 43 69 mulgnn0cld 
 |-  ( ph -> ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` M ) )
71 eqid 
 |-  ( Base ` M ) = ( Base ` M )
72 22 crngmgp 
 |-  ( ( Poly1 ` K ) e. CRing -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
73 19 72 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
74 15 73 eqeltrid 
 |-  ( ph -> M e. CMnd )
75 fzfid 
 |-  ( ph -> ( 0 ... A ) e. Fin )
76 diffi 
 |-  ( ( 0 ... A ) e. Fin -> ( ( 0 ... A ) \ { W } ) e. Fin )
77 75 76 syl 
 |-  ( ph -> ( ( 0 ... A ) \ { W } ) e. Fin )
78 24 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
79 32 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> Y : ( 0 ... A ) --> NN0 )
80 eldifi 
 |-  ( i e. ( ( 0 ... A ) \ { W } ) -> i e. ( 0 ... A ) )
81 80 adantl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> i e. ( 0 ... A ) )
82 79 81 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Y ` i ) e. NN0 )
83 46 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( Poly1 ` K ) e. Mnd )
84 51 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> X e. ( Base ` ( Poly1 ` K ) ) )
85 48 adantr 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> K e. Ring )
86 85 53 57 3syl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
87 elfzelz 
 |-  ( i e. ( 0 ... A ) -> i e. ZZ )
88 81 87 syl 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> i e. ZZ )
89 86 88 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
90 17 14 56 49 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) ) -> ( S ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
91 85 89 90 syl2anc 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( S ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
92 49 63 mndcl 
 |-  ( ( ( Poly1 ` K ) e. Mnd /\ X e. ( Base ` ( Poly1 ` K ) ) /\ ( S ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
93 83 84 91 92 syl3anc 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
94 93 68 eleqtrrdi 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` M ) )
95 26 7 mulgnn0cl 
 |-  ( ( ( mulGrp ` ( Poly1 ` K ) ) e. Mnd /\ ( Y ` i ) e. NN0 /\ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` M ) ) -> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` M ) )
96 78 82 94 95 syl3anc 
 |-  ( ( ph /\ i e. ( ( 0 ... A ) \ { W } ) ) -> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` M ) )
97 96 ralrimiva 
 |-  ( ph -> A. i e. ( ( 0 ... A ) \ { W } ) ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` M ) )
98 71 74 77 97 gsummptcl 
 |-  ( ph -> ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` M ) )
99 eqid 
 |-  ( +g ` M ) = ( +g ` M )
100 71 99 mndcl 
 |-  ( ( M e. Mnd /\ ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` M ) /\ ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` M ) ) -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` M ) )
101 25 70 98 100 syl3anc 
 |-  ( ph -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` M ) )
102 101 68 eleqtrdi 
 |-  ( ph -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
103 71 99 cmncom 
 |-  ( ( M e. CMnd /\ ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` M ) /\ ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` M ) ) -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
104 74 70 98 103 syl3anc 
 |-  ( ph -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
105 104 oveq1d 
 |-  ( ph -> ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
106 eqid 
 |-  ( .r ` ( Poly1 ` K ) ) = ( .r ` ( Poly1 ` K ) )
107 15 106 mgpplusg 
 |-  ( .r ` ( Poly1 ` K ) ) = ( +g ` M )
108 107 eqcomi 
 |-  ( +g ` M ) = ( .r ` ( Poly1 ` K ) )
109 108 a1i 
 |-  ( ph -> ( +g ` M ) = ( .r ` ( Poly1 ` K ) ) )
110 109 oveqd 
 |-  ( ph -> ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
111 110 oveq1d 
 |-  ( ph -> ( ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
112 98 68 eleqtrdi 
 |-  ( ph -> ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
113 70 68 eleqtrdi 
 |-  ( ph -> ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
114 66 7 24 11 65 mulgnn0cld 
 |-  ( ph -> ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
115 49 106 21 112 113 114 ringassd 
 |-  ( ph -> ( ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) )
116 111 115 eqtrd 
 |-  ( ph -> ( ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( +g ` M ) ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) )
117 105 116 eqtrd 
 |-  ( ph -> ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) )
118 117 oveq2d 
 |-  ( ph -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) = ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) )
119 37 recnd 
 |-  ( ph -> ( Y ` W ) e. CC )
120 38 recnd 
 |-  ( ph -> C e. CC )
121 119 120 npcand 
 |-  ( ph -> ( ( ( Y ` W ) - C ) + C ) = ( Y ` W ) )
122 121 eqcomd 
 |-  ( ph -> ( Y ` W ) = ( ( ( Y ` W ) - C ) + C ) )
123 122 oveq1d 
 |-  ( ph -> ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( ( ( ( Y ` W ) - C ) + C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) )
124 66 a1i 
 |-  ( ph -> ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
125 65 124 eleqtrd 
 |-  ( ph -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
126 43 11 125 3jca 
 |-  ( ph -> ( ( ( Y ` W ) - C ) e. NN0 /\ C e. NN0 /\ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) ) )
127 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
128 22 106 mgpplusg 
 |-  ( .r ` ( Poly1 ` K ) ) = ( +g ` ( mulGrp ` ( Poly1 ` K ) ) )
129 127 7 128 mulgnn0dir 
 |-  ( ( ( mulGrp ` ( Poly1 ` K ) ) e. Mnd /\ ( ( ( Y ` W ) - C ) e. NN0 /\ C e. NN0 /\ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) ) ) -> ( ( ( ( Y ` W ) - C ) + C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
130 24 126 129 syl2anc 
 |-  ( ph -> ( ( ( ( Y ` W ) - C ) + C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
131 123 130 eqtr2d 
 |-  ( ph -> ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) )
132 131 oveq2d 
 |-  ( ph -> ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
133 8 a1i 
 |-  ( ph -> 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 ) ) ) ) ) ) ) )
134 15 eqcomi 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = M
135 134 a1i 
 |-  ( ( ph /\ g = Y ) -> ( mulGrp ` ( Poly1 ` K ) ) = M )
136 simplr 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> g = Y )
137 136 fveq1d 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> ( g ` i ) = ( Y ` i ) )
138 14 eqcomi 
 |-  ( algSc ` ( Poly1 ` K ) ) = S
139 138 a1i 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> ( algSc ` ( Poly1 ` K ) ) = S )
140 139 fveq1d 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) = ( S ` ( ( ZRHom ` K ) ` i ) ) )
141 140 oveq2d 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) = ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) )
142 137 141 oveq12d 
 |-  ( ( ( ph /\ g = Y ) /\ i e. ( 0 ... A ) ) -> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) )
143 142 mpteq2dva 
 |-  ( ( ph /\ g = Y ) -> ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
144 135 143 oveq12d 
 |-  ( ( ph /\ g = Y ) -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( M gsum ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
145 ovexd 
 |-  ( ph -> ( M gsum ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. _V )
146 133 144 9 145 fvmptd 
 |-  ( ph -> ( G ` Y ) = ( M gsum ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
147 10 snssd 
 |-  ( ph -> { W } C_ ( 0 ... A ) )
148 undifr 
 |-  ( { W } C_ ( 0 ... A ) <-> ( ( ( 0 ... A ) \ { W } ) u. { W } ) = ( 0 ... A ) )
149 147 148 sylib 
 |-  ( ph -> ( ( ( 0 ... A ) \ { W } ) u. { W } ) = ( 0 ... A ) )
150 149 eqcomd 
 |-  ( ph -> ( 0 ... A ) = ( ( ( 0 ... A ) \ { W } ) u. { W } ) )
151 150 mpteq1d 
 |-  ( ph -> ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( ( ( 0 ... A ) \ { W } ) u. { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
152 151 oveq2d 
 |-  ( ph -> ( M gsum ( i e. ( 0 ... A ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( M gsum ( i e. ( ( ( 0 ... A ) \ { W } ) u. { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
153 146 152 eqtrd 
 |-  ( ph -> ( G ` Y ) = ( M gsum ( i e. ( ( ( 0 ... A ) \ { W } ) u. { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
154 neldifsnd 
 |-  ( ph -> -. W e. ( ( 0 ... A ) \ { W } ) )
155 26 7 24 33 69 mulgnn0cld 
 |-  ( ph -> ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` M ) )
156 fveq2 
 |-  ( i = W -> ( Y ` i ) = ( Y ` W ) )
157 2fveq3 
 |-  ( i = W -> ( S ` ( ( ZRHom ` K ) ` i ) ) = ( S ` ( ( ZRHom ` K ) ` W ) ) )
158 157 oveq2d 
 |-  ( i = W -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) = ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) )
159 156 158 oveq12d 
 |-  ( i = W -> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) )
160 71 107 74 77 96 10 154 155 159 gsumunsn 
 |-  ( ph -> ( M gsum ( i e. ( ( ( 0 ... A ) \ { W } ) u. { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
161 153 160 eqtr2d 
 |-  ( ph -> ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( Y ` W ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( G ` Y ) )
162 132 161 eqtrd 
 |-  ( ph -> ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) = ( G ` Y ) )
163 162 oveq2d 
 |-  ( ph -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) = ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( G ` Y ) ) )
164 21 ringgrpd 
 |-  ( ph -> ( Poly1 ` K ) e. Grp )
165 1 2 3 4 5 6 7 8 aks6d1c5lem0 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
166 165 9 ffvelcdmd 
 |-  ( ph -> ( G ` Y ) e. ( Base ` ( Poly1 ` K ) ) )
167 eqid 
 |-  ( 0g ` ( Poly1 ` K ) ) = ( 0g ` ( Poly1 ` K ) )
168 eqid 
 |-  ( -g ` ( Poly1 ` K ) ) = ( -g ` ( Poly1 ` K ) )
169 49 167 168 grpsubid 
 |-  ( ( ( Poly1 ` K ) e. Grp /\ ( G ` Y ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( G ` Y ) ) = ( 0g ` ( Poly1 ` K ) ) )
170 164 166 169 syl2anc 
 |-  ( ph -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( G ` Y ) ) = ( 0g ` ( Poly1 ` K ) ) )
171 163 170 eqtrd 
 |-  ( ph -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) = ( 0g ` ( Poly1 ` K ) ) )
172 118 171 eqtrd 
 |-  ( ph -> ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) = ( 0g ` ( Poly1 ` K ) ) )
173 172 fveq2d 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) = ( ( deg1 ` K ) ` ( 0g ` ( Poly1 ` K ) ) ) )
174 eqid 
 |-  ( deg1 ` K ) = ( deg1 ` K )
175 174 17 167 deg1z 
 |-  ( K e. Ring -> ( ( deg1 ` K ) ` ( 0g ` ( Poly1 ` K ) ) ) = -oo )
176 48 175 syl 
 |-  ( ph -> ( ( deg1 ` K ) ` ( 0g ` ( Poly1 ` K ) ) ) = -oo )
177 1 flddrngd 
 |-  ( ph -> K e. DivRing )
178 drngdomn 
 |-  ( K e. DivRing -> K e. Domn )
179 177 178 syl 
 |-  ( ph -> K e. Domn )
180 17 ply1domn 
 |-  ( K e. Domn -> ( Poly1 ` K ) e. Domn )
181 179 180 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Domn )
182 19 181 jca 
 |-  ( ph -> ( ( Poly1 ` K ) e. CRing /\ ( Poly1 ` K ) e. Domn ) )
183 isidom 
 |-  ( ( Poly1 ` K ) e. IDomn <-> ( ( Poly1 ` K ) e. CRing /\ ( Poly1 ` K ) e. Domn ) )
184 182 183 sylibr 
 |-  ( ph -> ( Poly1 ` K ) e. IDomn )
185 174 17 49 deg1xrcl 
 |-  ( ( S ` ( ( ZRHom ` K ) ` W ) ) e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. RR* )
186 62 185 syl 
 |-  ( ph -> ( ( deg1 ` K ) ` ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. RR* )
187 0xr 
 |-  0 e. RR*
188 187 a1i 
 |-  ( ph -> 0 e. RR* )
189 174 17 49 deg1xrcl 
 |-  ( X e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` X ) e. RR* )
190 51 189 syl 
 |-  ( ph -> ( ( deg1 ` K ) ` X ) e. RR* )
191 174 17 56 14 deg1sclle 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` W ) e. ( Base ` K ) ) -> ( ( deg1 ` K ) ` ( S ` ( ( ZRHom ` K ) ` W ) ) ) <_ 0 )
192 48 60 191 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( S ` ( ( ZRHom ` K ) ` W ) ) ) <_ 0 )
193 0lt1 
 |-  0 < 1
194 193 a1i 
 |-  ( ph -> 0 < 1 )
195 51 66 eleqtrdi 
 |-  ( ph -> X e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
196 127 7 mulg1 
 |-  ( X e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) -> ( 1 .^ X ) = X )
197 195 196 syl 
 |-  ( ph -> ( 1 .^ X ) = X )
198 197 fveq2d 
 |-  ( ph -> ( ( deg1 ` K ) ` ( 1 .^ X ) ) = ( ( deg1 ` K ) ` X ) )
199 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
200 199 biimpi 
 |-  ( K e. Field -> ( K e. DivRing /\ K e. CRing ) )
201 1 200 syl 
 |-  ( ph -> ( K e. DivRing /\ K e. CRing ) )
202 201 simpld 
 |-  ( ph -> K e. DivRing )
203 drngnzr 
 |-  ( K e. DivRing -> K e. NzRing )
204 202 203 syl 
 |-  ( ph -> K e. NzRing )
205 1nn0 
 |-  1 e. NN0
206 205 a1i 
 |-  ( ph -> 1 e. NN0 )
207 174 17 6 22 7 deg1pw 
 |-  ( ( K e. NzRing /\ 1 e. NN0 ) -> ( ( deg1 ` K ) ` ( 1 .^ X ) ) = 1 )
208 204 206 207 syl2anc 
 |-  ( ph -> ( ( deg1 ` K ) ` ( 1 .^ X ) ) = 1 )
209 198 208 eqtr3d 
 |-  ( ph -> ( ( deg1 ` K ) ` X ) = 1 )
210 209 eqcomd 
 |-  ( ph -> 1 = ( ( deg1 ` K ) ` X ) )
211 194 210 breqtrd 
 |-  ( ph -> 0 < ( ( deg1 ` K ) ` X ) )
212 186 188 190 192 211 xrlelttrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( S ` ( ( ZRHom ` K ) ` W ) ) ) < ( ( deg1 ` K ) ` X ) )
213 17 174 48 49 63 51 62 212 deg1add 
 |-  ( ph -> ( ( deg1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) = ( ( deg1 ` K ) ` X ) )
214 209 206 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` X ) e. NN0 )
215 213 214 eqeltrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. NN0 )
216 174 17 167 49 deg1nn0clb 
 |-  ( ( K e. Ring /\ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. NN0 ) )
217 48 65 216 syl2anc 
 |-  ( ph -> ( ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. NN0 ) )
218 215 217 mpbird 
 |-  ( ph -> ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
219 184 65 218 11 7 idomnnzpownz 
 |-  ( ph -> ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
220 174 17 167 49 deg1nn0clb 
 |-  ( ( K e. Ring /\ ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) e. NN0 ) )
221 48 114 220 syl2anc 
 |-  ( ph -> ( ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) e. NN0 ) )
222 219 221 mpbid 
 |-  ( ph -> ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) e. NN0 )
223 222 nn0red 
 |-  ( ph -> ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) e. RR )
224 223 mnfltd 
 |-  ( ph -> -oo < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
225 176 224 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( 0g ` ( Poly1 ` K ) ) ) < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
226 173 225 eqbrtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) )
227 102 226 jca 
 |-  ( ph -> ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( deg1 ` K ) ` ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) )
228 eqid 
 |-  ( Unic1p ` K ) = ( Unic1p ` K )
229 17 49 167 228 drnguc1p 
 |-  ( ( K e. DivRing /\ ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) ) -> ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Unic1p ` K ) )
230 177 114 219 229 syl3anc 
 |-  ( ph -> ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Unic1p ` K ) )
231 13 17 49 174 168 106 228 q1peqb 
 |-  ( ( K e. Ring /\ ( G ` Y ) e. ( Base ` ( Poly1 ` K ) ) /\ ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) e. ( Unic1p ` K ) ) -> ( ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( deg1 ` K ) ` ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) <-> ( ( G ` Y ) Q ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) )
232 48 166 230 231 syl3anc 
 |-  ( ph -> ( ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( deg1 ` K ) ` ( ( G ` Y ) ( -g ` ( Poly1 ` K ) ) ( ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ( .r ` ( Poly1 ` K ) ) ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) ) < ( ( deg1 ` K ) ` ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) ) <-> ( ( G ` Y ) Q ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) )
233 227 232 mpbid 
 |-  ( ph -> ( ( G ` Y ) Q ( C .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ) = ( ( ( ( Y ` W ) - C ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` W ) ) ) ) ( +g ` M ) ( M gsum ( i e. ( ( 0 ... A ) \ { W } ) |-> ( ( Y ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( S ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )