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 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
Assertion aks6d1c5 ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) –1-1→ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
4 aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
5 aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
6 aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
7 aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
8 aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
9 eqid ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
10 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
11 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
12 11 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
13 10 12 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
14 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
15 14 crngmgp ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CRing → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
16 13 15 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ CMnd )
18 fzfid ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( 0 ... 𝐴 ) ∈ Fin )
19 17 cmnmndd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ∈ Mnd )
21 nn0ex ⊢ ℕ0 ∈ V
22 21 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
23 ovexd ⊢ ( 𝜑 → ( 0 ... 𝐴 ) ∈ V )
24 22 23 elmapd ⊢ ( 𝜑 → ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
25 24 biimpd ⊢ ( 𝜑 → ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) → 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
26 25 imp ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → 𝑔 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
27 26 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑔 ‘ 𝑖 ) ∈ ℕ0 )
28 13 crngringd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
29 28 ringcmnd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CMnd )
30 cmnmnd ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ CMnd → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
31 29 30 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( Poly1 ‘ 𝐾 ) ∈ Mnd )
34 10 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → 𝐾 ∈ Ring )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝐾 ∈ Ring )
37 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
38 6 11 37 vr1cl ⊢ ( 𝐾 ∈ Ring → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
39 36 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
40 simpl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) )
41 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝐴 ) → 𝑖 ∈ ℤ )
42 41 adantl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → 𝑖 ∈ ℤ )
43 40 42 jca ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ℤ ) )
44 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
45 44 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
46 zringbas ⊢ ℤ = ( Base ‘ ℤring )
47 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
48 46 47 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
49 45 48 syl ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
50 35 49 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
51 50 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ℤ ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
52 43 51 syl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) )
53 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
54 11 53 47 37 ply1sclcl ⊢ ( ( 𝐾 ∈ Ring ∧ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
55 36 52 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
56 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
57 37 56 mndcl ⊢ ( ( ( Poly1 ‘ 𝐾 ) ∈ Mnd ∧ 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
58 33 39 55 57 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
59 14 37 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
60 59 a1i ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
61 58 60 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
62 9 7 20 27 61 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
63 62 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ∀ 𝑖 ∈ ( 0 ... 𝐴 ) ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
64 9 17 18 63 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
65 59 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
67 64 66 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
68 67 8 fmptd ⊢ ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
69 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 ) )
70 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
71 70 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ 𝑥 = 𝑦 )
72 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
73 21 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ℕ0 ∈ V )
74 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 0 ... 𝐴 ) ∈ V )
75 73 74 elmapd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑥 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
76 72 75 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
77 ffn ⊢ ( 𝑥 : ( 0 ... 𝐴 ) ⟶ ℕ0 → 𝑥 Fn ( 0 ... 𝐴 ) )
78 76 77 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 Fn ( 0 ... 𝐴 ) )
79 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
80 73 74 elmapd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↔ 𝑦 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
81 79 80 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
82 ffn ⊢ ( 𝑦 : ( 0 ... 𝐴 ) ⟶ ℕ0 → 𝑦 Fn ( 0 ... 𝐴 ) )
83 81 82 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 Fn ( 0 ... 𝐴 ) )
84 eqfnfv2 ⊢ ( ( 𝑥 Fn ( 0 ... 𝐴 ) ∧ 𝑦 Fn ( 0 ... 𝐴 ) ) → ( 𝑥 = 𝑦 ↔ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) ) )
85 78 83 84 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 = 𝑦 ↔ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) ) )
86 85 notbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ¬ 𝑥 = 𝑦 ↔ ¬ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) ) )
87 86 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ¬ 𝑥 = 𝑦 → ¬ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) ) )
88 71 87 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) )
89 ianor ⊢ ( ¬ ( ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∧ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) ↔ ( ¬ ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∨ ¬ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) )
90 88 89 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( ¬ ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) ∨ ¬ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ) )
91 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) )
92 91 notnotd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ¬ ( 0 ... 𝐴 ) = ( 0 ... 𝐴 ) )
93 90 92 orcnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
94 rexnal ⊢ ( ∃ 𝑧 ∈ ( 0 ... 𝐴 ) ¬ ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) ↔ ¬ ∀ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
95 93 94 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑧 ∈ ( 0 ... 𝐴 ) ¬ ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
96 df-ne ⊢ ( ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ↔ ¬ ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
97 96 rexbii ⊢ ( ∃ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ ( 0 ... 𝐴 ) ¬ ( 𝑥 ‘ 𝑧 ) = ( 𝑦 ‘ 𝑧 ) )
98 95 97 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑧 ∈ ( 0 ... 𝐴 ) ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) )
99 simpl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑧 ∈ ( 0 ... 𝐴 ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) )
100 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑧 ∈ ( 0 ... 𝐴 ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) ) → 𝑧 ∈ ( 0 ... 𝐴 ) )
101 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑧 ∈ ( 0 ... 𝐴 ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) ) → ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) )
102 99 100 101 jca31 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑧 ∈ ( 0 ... 𝐴 ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) ) → ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) )
103 75 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) → 𝑥 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
104 72 103 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
105 104 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( 𝑥 ‘ 𝑧 ) ∈ ℕ0 )
106 105 nn0red ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( 𝑥 ‘ 𝑧 ) ∈ ℝ )
107 80 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) → 𝑦 : ( 0 ... 𝐴 ) ⟶ ℕ0 ) )
108 79 107 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 : ( 0 ... 𝐴 ) ⟶ ℕ0 )
109 108 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ℕ0 )
110 109 nn0red ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( 𝑦 ‘ 𝑧 ) ∈ ℝ )
111 106 110 lttri2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ↔ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∨ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) ) )
112 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝐾 ∈ Field )
113 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝑃 ∈ ℙ )
114 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝐴 ∈ ℕ0 )
115 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝐴 < 𝑃 )
116 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
117 79 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
118 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
119 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → 𝑧 ∈ ( 0 ... 𝐴 ) )
120 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) )
121 112 113 3 114 115 6 7 8 116 117 118 119 120 aks6d1c5lem2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
122 1 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝐾 ∈ Field )
123 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝑃 ∈ ℙ )
124 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝐴 ∈ ℕ0 )
125 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝐴 < 𝑃 )
126 79 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
127 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) )
128 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
129 128 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) )
130 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → 𝑧 ∈ ( 0 ... 𝐴 ) )
131 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) )
132 122 123 3 124 125 6 7 8 126 127 129 130 131 aks6d1c5lem2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
133 121 132 jaodan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∨ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
134 133 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∨ ( 𝑦 ‘ 𝑧 ) < ( 𝑥 ‘ 𝑧 ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) ) )
135 111 134 sylbid ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) → ( ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) ) )
136 135 imp ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑧 ∈ ( 0 ... 𝐴 ) ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
137 102 136 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ∧ ( 𝑧 ∈ ( 0 ... 𝐴 ) ∧ ( 𝑥 ‘ 𝑧 ) ≠ ( 𝑦 ‘ 𝑧 ) ) ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
138 98 137 rexlimddv ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ( 0g ‘ 𝐾 ) ≠ ( 0g ‘ 𝐾 ) )
139 138 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 ) )
140 69 139 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) → ¬ 𝑥 ≠ 𝑦 )
141 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
142 141 notbii ⊢ ( ¬ 𝑥 ≠ 𝑦 ↔ ¬ ¬ 𝑥 = 𝑦 )
143 140 142 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) → ¬ ¬ 𝑥 = 𝑦 )
144 notnotb ⊢ ( 𝑥 = 𝑦 ↔ ¬ ¬ 𝑥 = 𝑦 )
145 143 144 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
146 145 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ∧ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
147 146 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) → ∀ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
148 147 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∀ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
149 68 148 jca ⊢ ( 𝜑 → ( 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∀ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
150 dff13 ⊢ ( 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) –1-1→ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↔ ( 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∀ 𝑦 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
151 149 150 sylibr ⊢ ( 𝜑 → 𝐺 : ( ℕ0 ↑m ( 0 ... 𝐴 ) ) –1-1→ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )