Metamath Proof Explorer

Theorem aks6d1c5

Description: Claim 5 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . The mapping defined by G is injective. (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 ) ) ) ) ) ) )
Assertion aks6d1c5 
|- ( ph -> G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` 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 eqid 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
10 1 fldcrngd 
 |-  ( ph -> K e. CRing )
11 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
12 11 ply1crng 
 |-  ( K e. CRing -> ( Poly1 ` K ) e. CRing )
13 10 12 syl 
 |-  ( ph -> ( Poly1 ` K ) e. CRing )
14 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
15 14 crngmgp 
 |-  ( ( Poly1 ` K ) e. CRing -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
16 13 15 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
17 16 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. CMnd )
18 fzfid 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( 0 ... A ) e. Fin )
19 17 cmnmndd 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
20 19 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
21 nn0ex 
 |-  NN0 e. _V
22 21 a1i 
 |-  ( ph -> NN0 e. _V )
23 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
24 22 23 elmapd 
 |-  ( ph -> ( g e. ( NN0 ^m ( 0 ... A ) ) <-> g : ( 0 ... A ) --> NN0 ) )
25 24 biimpd 
 |-  ( ph -> ( g e. ( NN0 ^m ( 0 ... A ) ) -> g : ( 0 ... A ) --> NN0 ) )
26 25 imp 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> g : ( 0 ... A ) --> NN0 )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( g ` i ) e. NN0 )
28 13 crngringd 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
29 28 ringcmnd 
 |-  ( ph -> ( Poly1 ` K ) e. CMnd )
30 cmnmnd 
 |-  ( ( Poly1 ` K ) e. CMnd -> ( Poly1 ` K ) e. Mnd )
31 29 30 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Mnd )
32 31 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( Poly1 ` K ) e. Mnd )
33 32 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( Poly1 ` K ) e. Mnd )
34 10 crngringd 
 |-  ( ph -> K e. Ring )
35 34 adantr 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> K e. Ring )
36 35 adantr 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> K e. Ring )
37 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
38 6 11 37 vr1cl 
 |-  ( K e. Ring -> X e. ( Base ` ( Poly1 ` K ) ) )
39 36 38 syl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> X e. ( Base ` ( Poly1 ` K ) ) )
40 simpl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) )
41 elfzelz 
 |-  ( i e. ( 0 ... A ) -> i e. ZZ )
42 41 adantl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> i e. ZZ )
43 40 42 jca 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ZZ ) )
44 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
45 44 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
46 zringbas 
 |-  ZZ = ( Base ` ZZring )
47 eqid 
 |-  ( Base ` K ) = ( Base ` K )
48 46 47 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
49 45 48 syl 
 |-  ( K e. Ring -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
50 35 49 syl 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
51 50 ffvelcdmda 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ZZ ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
52 43 51 syl 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) )
53 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
54 11 53 47 37 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` i ) e. ( Base ` K ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
55 36 52 54 syl2anc 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) e. ( Base ` ( Poly1 ` K ) ) )
56 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
57 37 56 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 ) ) )
58 33 39 55 57 syl3anc 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
59 14 37 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
60 59 a1i 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
61 58 60 eleqtrd 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
62 9 7 20 27 61 mulgnn0cld 
 |-  ( ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) /\ i e. ( 0 ... A ) ) -> ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
63 62 ralrimiva 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> A. i e. ( 0 ... A ) ( ( g ` i ) .^ ( X ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
64 9 17 18 63 gsummptcl 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) e. ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) )
65 59 eqcomi 
 |-  ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) )
66 65 a1i 
 |-  ( ( ph /\ g e. ( NN0 ^m ( 0 ... A ) ) ) -> ( Base ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( Base ` ( Poly1 ` K ) ) )
67 64 66 eleqtrd 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
68 67 8 fmptd 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) )
69 eqidd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( 0g ` K ) = ( 0g ` K ) )
70 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> x =/= y )
71 70 neneqd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> -. x = y )
72 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> x e. ( NN0 ^m ( 0 ... A ) ) )
73 21 a1i 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> NN0 e. _V )
74 ovexd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( 0 ... A ) e. _V )
75 73 74 elmapd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( x e. ( NN0 ^m ( 0 ... A ) ) <-> x : ( 0 ... A ) --> NN0 ) )
76 72 75 mpbid 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> x : ( 0 ... A ) --> NN0 )
77 ffn 
 |-  ( x : ( 0 ... A ) --> NN0 -> x Fn ( 0 ... A ) )
78 76 77 syl 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> x Fn ( 0 ... A ) )
79 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> y e. ( NN0 ^m ( 0 ... A ) ) )
80 73 74 elmapd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( y e. ( NN0 ^m ( 0 ... A ) ) <-> y : ( 0 ... A ) --> NN0 ) )
81 79 80 mpbid 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> y : ( 0 ... A ) --> NN0 )
82 ffn 
 |-  ( y : ( 0 ... A ) --> NN0 -> y Fn ( 0 ... A ) )
83 81 82 syl 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> y Fn ( 0 ... A ) )
84 eqfnfv2 
 |-  ( ( x Fn ( 0 ... A ) /\ y Fn ( 0 ... A ) ) -> ( x = y <-> ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) ) )
85 78 83 84 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( x = y <-> ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) ) )
86 85 notbid 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( -. x = y <-> -. ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) ) )
87 86 biimpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( -. x = y -> -. ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) ) )
88 71 87 mpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> -. ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) )
89 ianor 
 |-  ( -. ( ( 0 ... A ) = ( 0 ... A ) /\ A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) <-> ( -. ( 0 ... A ) = ( 0 ... A ) \/ -. A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) )
90 88 89 sylib 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( -. ( 0 ... A ) = ( 0 ... A ) \/ -. A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) ) )
91 eqidd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( 0 ... A ) = ( 0 ... A ) )
92 91 notnotd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> -. -. ( 0 ... A ) = ( 0 ... A ) )
93 90 92 orcnd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> -. A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) )
94 rexnal 
 |-  ( E. z e. ( 0 ... A ) -. ( x ` z ) = ( y ` z ) <-> -. A. z e. ( 0 ... A ) ( x ` z ) = ( y ` z ) )
95 93 94 sylibr 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> E. z e. ( 0 ... A ) -. ( x ` z ) = ( y ` z ) )
96 df-ne 
 |-  ( ( x ` z ) =/= ( y ` z ) <-> -. ( x ` z ) = ( y ` z ) )
97 96 rexbii 
 |-  ( E. z e. ( 0 ... A ) ( x ` z ) =/= ( y ` z ) <-> E. z e. ( 0 ... A ) -. ( x ` z ) = ( y ` z ) )
98 95 97 sylibr 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> E. z e. ( 0 ... A ) ( x ` z ) =/= ( y ` z ) )
99 simpl 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ ( z e. ( 0 ... A ) /\ ( x ` z ) =/= ( y ` z ) ) ) -> ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) )
100 simprl 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ ( z e. ( 0 ... A ) /\ ( x ` z ) =/= ( y ` z ) ) ) -> z e. ( 0 ... A ) )
101 simprr 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ ( z e. ( 0 ... A ) /\ ( x ` z ) =/= ( y ` z ) ) ) -> ( x ` z ) =/= ( y ` z ) )
102 99 100 101 jca31 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ ( z e. ( 0 ... A ) /\ ( x ` z ) =/= ( y ` z ) ) ) -> ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) =/= ( y ` z ) ) )
103 75 biimpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( x e. ( NN0 ^m ( 0 ... A ) ) -> x : ( 0 ... A ) --> NN0 ) )
104 72 103 mpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> x : ( 0 ... A ) --> NN0 )
105 104 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( x ` z ) e. NN0 )
106 105 nn0red 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( x ` z ) e. RR )
107 80 biimpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( y e. ( NN0 ^m ( 0 ... A ) ) -> y : ( 0 ... A ) --> NN0 ) )
108 79 107 mpd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> y : ( 0 ... A ) --> NN0 )
109 108 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( y ` z ) e. NN0 )
110 109 nn0red 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( y ` z ) e. RR )
111 106 110 lttri2d 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( ( x ` z ) =/= ( y ` z ) <-> ( ( x ` z ) < ( y ` z ) \/ ( y ` z ) < ( x ` z ) ) ) )
112 1 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> K e. Field )
113 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> P e. Prime )
114 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> A e. NN0 )
115 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> A < P )
116 72 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> x e. ( NN0 ^m ( 0 ... A ) ) )
117 79 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> y e. ( NN0 ^m ( 0 ... A ) ) )
118 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> ( G ` x ) = ( G ` y ) )
119 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> z e. ( 0 ... A ) )
120 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> ( x ` z ) < ( y ` z ) )
121 112 113 3 114 115 6 7 8 116 117 118 119 120 aks6d1c5lem2 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) < ( y ` z ) ) -> ( 0g ` K ) =/= ( 0g ` K ) )
122 1 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> K e. Field )
123 2 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> P e. Prime )
124 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> A e. NN0 )
125 5 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> A < P )
126 79 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> y e. ( NN0 ^m ( 0 ... A ) ) )
127 72 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> x e. ( NN0 ^m ( 0 ... A ) ) )
128 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> ( G ` x ) = ( G ` y ) )
129 128 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> ( G ` y ) = ( G ` x ) )
130 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> z e. ( 0 ... A ) )
131 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> ( y ` z ) < ( x ` z ) )
132 122 123 3 124 125 6 7 8 126 127 129 130 131 aks6d1c5lem2 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( y ` z ) < ( x ` z ) ) -> ( 0g ` K ) =/= ( 0g ` K ) )
133 121 132 jaodan 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( ( x ` z ) < ( y ` z ) \/ ( y ` z ) < ( x ` z ) ) ) -> ( 0g ` K ) =/= ( 0g ` K ) )
134 133 ex 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( ( ( x ` z ) < ( y ` z ) \/ ( y ` z ) < ( x ` z ) ) -> ( 0g ` K ) =/= ( 0g ` K ) ) )
135 111 134 sylbid 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) -> ( ( x ` z ) =/= ( y ` z ) -> ( 0g ` K ) =/= ( 0g ` K ) ) )
136 135 imp 
 |-  ( ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ z e. ( 0 ... A ) ) /\ ( x ` z ) =/= ( y ` z ) ) -> ( 0g ` K ) =/= ( 0g ` K ) )
137 102 136 syl 
 |-  ( ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) /\ ( z e. ( 0 ... A ) /\ ( x ` z ) =/= ( y ` z ) ) ) -> ( 0g ` K ) =/= ( 0g ` K ) )
138 98 137 rexlimddv 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> ( 0g ` K ) =/= ( 0g ` K ) )
139 138 neneqd 
 |-  ( ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) /\ x =/= y ) -> -. ( 0g ` K ) = ( 0g ` K ) )
140 69 139 pm2.65da 
 |-  ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) -> -. x =/= y )
141 df-ne 
 |-  ( x =/= y <-> -. x = y )
142 141 notbii 
 |-  ( -. x =/= y <-> -. -. x = y )
143 140 142 sylib 
 |-  ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) -> -. -. x = y )
144 notnotb 
 |-  ( x = y <-> -. -. x = y )
145 143 144 sylibr 
 |-  ( ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) /\ ( G ` x ) = ( G ` y ) ) -> x = y )
146 145 ex 
 |-  ( ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) /\ y e. ( NN0 ^m ( 0 ... A ) ) ) -> ( ( G ` x ) = ( G ` y ) -> x = y ) )
147 146 ralrimiva 
 |-  ( ( ph /\ x e. ( NN0 ^m ( 0 ... A ) ) ) -> A. y e. ( NN0 ^m ( 0 ... A ) ) ( ( G ` x ) = ( G ` y ) -> x = y ) )
148 147 ralrimiva 
 |-  ( ph -> A. x e. ( NN0 ^m ( 0 ... A ) ) A. y e. ( NN0 ^m ( 0 ... A ) ) ( ( G ` x ) = ( G ` y ) -> x = y ) )
149 68 148 jca 
 |-  ( ph -> ( G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) /\ A. x e. ( NN0 ^m ( 0 ... A ) ) A. y e. ( NN0 ^m ( 0 ... A ) ) ( ( G ` x ) = ( G ` y ) -> x = y ) ) )
150 dff13 
 |-  ( G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) <-> ( G : ( NN0 ^m ( 0 ... A ) ) --> ( Base ` ( Poly1 ` K ) ) /\ A. x e. ( NN0 ^m ( 0 ... A ) ) A. y e. ( NN0 ^m ( 0 ... A ) ) ( ( G ` x ) = ( G ` y ) -> x = y ) ) )
151 149 150 sylibr 
 |-  ( ph -> G : ( NN0 ^m ( 0 ... A ) ) -1-1-> ( Base ` ( Poly1 ` K ) ) )