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