| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks6d1c1p2.13 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 2 |  | isfld 20741 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ Field ↔ (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) | 
| 3 | 1, 2 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing)) | 
| 4 | 3 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ CRing) | 
| 5 |  | aks6d1c1p2.6 | . . . . . . . . . . . . 13
⊢ 𝑉 = (mulGrp‘𝐾) | 
| 6 | 5 | crngmgp 20239 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd) | 
| 7 | 4, 6 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ∈ CMnd) | 
| 8 |  | aks6d1c1p2.15 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 9 | 8 | nnnn0d 12589 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈
ℕ0) | 
| 10 |  | aks6d1c1p2.7 | . . . . . . . . . . 11
⊢  ↑ =
(.g‘𝑉) | 
| 11 | 7, 9, 10 | isprimroot 42095 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) ↔ (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑙)))) | 
| 12 | 11 | biimpd 229 | . . . . . . . . 9
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑙)))) | 
| 13 | 12 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅 ↑ 𝑦) = (0g‘𝑉) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑙))) | 
| 14 | 13 | simp1d 1142 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝑉)) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 16 | 5, 15 | mgpbas 20143 | . . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝑉) | 
| 17 | 16 | eqcomi 2745 | . . . . . . . . . 10
⊢
(Base‘𝑉) =
(Base‘𝐾) | 
| 18 | 17 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (Base‘𝑉) = (Base‘𝐾)) | 
| 19 | 18 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (Base‘𝑉) = (Base‘𝐾)) | 
| 20 | 19 | eleq2d 2826 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ↔ 𝑦 ∈ (Base‘𝐾))) | 
| 21 | 14, 20 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝐾)) | 
| 22 | 21 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → 𝑦 ∈ (Base‘𝐾))) | 
| 23 |  | aks6d1c1p2.18 | . . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))) | 
| 25 | 24 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑂‘𝐹) = (𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))) | 
| 26 | 25 | fveq1d 6907 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘𝑦) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) | 
| 27 | 26 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝑃 ↑ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦))) | 
| 28 |  | aks6d1c1p2.11 | . . . . . . . . . . . . 13
⊢ 𝑂 = (eval1‘𝐾) | 
| 29 |  | aks6d1c1p2.2 | . . . . . . . . . . . . 13
⊢ 𝑆 = (Poly1‘𝐾) | 
| 30 |  | aks6d1c1p2.3 | . . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑆) | 
| 31 | 4 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝐾 ∈ CRing) | 
| 32 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝐾)) | 
| 33 |  | crngring 20243 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring) | 
| 34 |  | aks6d1c1p2.4 | . . . . . . . . . . . . . . . 16
⊢ 𝑋 = (var1‘𝐾) | 
| 35 | 34, 29, 30 | vr1cl 22220 | . . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Ring → 𝑋 ∈ 𝐵) | 
| 36 | 31, 33, 35 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑋 ∈ 𝐵) | 
| 37 | 28, 34, 15, 29, 30, 31, 32 | evl1vard 22342 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑦) = 𝑦)) | 
| 38 | 37 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝑋)‘𝑦) = 𝑦) | 
| 39 | 36, 38 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑦) = 𝑦)) | 
| 40 | 4, 33 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 41 | 4 | crngringd 20244 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 42 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(ℤRHom‘𝐾) = (ℤRHom‘𝐾) | 
| 43 | 42 | zrhrhm 21523 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ Ring →
(ℤRHom‘𝐾)
∈ (ℤring RingHom 𝐾)) | 
| 44 |  | rhmghm 20485 | . . . . . . . . . . . . . . . . . 18
⊢
((ℤRHom‘𝐾) ∈ (ℤring RingHom
𝐾) →
(ℤRHom‘𝐾)
∈ (ℤring GrpHom 𝐾)) | 
| 45 |  | zringbas 21465 | . . . . . . . . . . . . . . . . . . 19
⊢ ℤ =
(Base‘ℤring) | 
| 46 | 45, 15 | ghmf 19239 | . . . . . . . . . . . . . . . . . 18
⊢
((ℤRHom‘𝐾) ∈ (ℤring GrpHom
𝐾) →
(ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 47 | 41, 43, 44, 46 | 4syl 19 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾)) | 
| 48 |  | aks6d1c1p2.19 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 49 | 47, 48 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾)) | 
| 50 |  | aks6d1c1p2.8 | . . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (algSc‘𝑆) | 
| 51 | 29, 50, 15, 30 | ply1sclcl 22290 | . . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ Ring ∧
((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) | 
| 52 | 40, 49, 51 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) | 
| 54 | 49 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((ℤRHom‘𝐾)‘𝐴) ∈ (Base‘𝐾)) | 
| 55 | 28, 29, 15, 50, 30, 31, 54, 32 | evl1scad 22340 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴))) | 
| 56 | 55 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴)) | 
| 57 | 53, 56 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘𝑦) = ((ℤRHom‘𝐾)‘𝐴))) | 
| 58 |  | aks6d1c1p2.12 | . . . . . . . . . . . . 13
⊢  + =
(+g‘𝑆) | 
| 59 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(+g‘𝐾) = (+g‘𝐾) | 
| 60 | 28, 29, 15, 30, 31, 32, 39, 57, 58, 59 | evl1addd 22346 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 61 | 60 | simprd 495 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 63 | 27, 62 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 64 | 25 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦))) | 
| 65 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝑉) =
(Base‘𝑉) | 
| 66 | 5 | ringmgp 20237 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ Ring → 𝑉 ∈ Mnd) | 
| 67 | 31, 33, 66 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑉 ∈ Mnd) | 
| 68 |  | aks6d1c1p2.14 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 69 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 71 | 70 | nnnn0d 12589 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑃 ∈
ℕ0) | 
| 73 | 32, 16 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝑉)) | 
| 74 | 65, 10, 67, 72, 73 | mulgnn0cld 19114 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝑉)) | 
| 75 | 74, 17 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ 𝑦) ∈ (Base‘𝐾)) | 
| 76 | 28, 34, 15, 29, 30, 31, 75 | evl1vard 22342 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ 𝑦))) | 
| 77 | 28, 29, 15, 50, 30, 31, 54, 75 | evl1scad 22340 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴))) | 
| 78 | 77 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴)) | 
| 79 | 53, 78 | jca 511 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘((ℤRHom‘𝐾)‘𝐴)))‘(𝑃 ↑ 𝑦)) = ((ℤRHom‘𝐾)‘𝐴))) | 
| 80 | 28, 29, 15, 30, 31, 75, 76, 79, 58, 59 | evl1addd 22346 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 81 | 80 | simprd 495 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 82 | 64, 81 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 83 |  | aks6d1c1p2.9 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = (.g‘𝑊) | 
| 84 |  | aks6d1c1p2.5 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑊 = (mulGrp‘𝑆) | 
| 85 | 84 | fveq2i 6908 | . . . . . . . . . . . . . . . . . 18
⊢
(.g‘𝑊) = (.g‘(mulGrp‘𝑆)) | 
| 86 | 83, 85 | eqtri 2764 | . . . . . . . . . . . . . . . . 17
⊢ 𝐷 =
(.g‘(mulGrp‘𝑆)) | 
| 87 | 5 | fveq2i 6908 | . . . . . . . . . . . . . . . . . 18
⊢
(.g‘𝑉) = (.g‘(mulGrp‘𝐾)) | 
| 88 | 10, 87 | eqtri 2764 | . . . . . . . . . . . . . . . . 17
⊢  ↑ =
(.g‘(mulGrp‘𝐾)) | 
| 89 | 28, 29, 15, 30, 31, 32, 37, 86, 88, 72 | evl1expd 22350 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷𝑋) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷𝑋))‘𝑦) = (𝑃 ↑ 𝑦))) | 
| 90 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(+g‘𝑆) = (+g‘𝑆) | 
| 91 | 28, 29, 15, 30, 31, 32, 89, 57, 90, 59 | evl1addd 22346 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 92 | 91 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 93 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 94 | 92, 93 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) | 
| 95 | 94 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) | 
| 96 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) = (𝐶‘((ℤRHom‘𝐾)‘𝐴)) | 
| 97 |  | aks6d1c1p2.10 | . . . . . . . . . . . . . . . . 17
⊢ 𝑃 = (chr‘𝐾) | 
| 98 | 29, 34, 90, 84, 83, 50, 96, 97, 4, 68, 48 | ply1fermltlchr 22317 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) = ((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) | 
| 99 | 98 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))) = (𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))) | 
| 100 | 99 | fveq1d 6907 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦)) | 
| 101 | 100 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦)) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘((𝑃𝐷𝑋)(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = ((𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦)) | 
| 103 | 28, 29, 15, 30, 31, 32, 37, 55, 90, 59 | evl1addd 22346 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵 ∧ ((𝑂‘(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴))))‘𝑦) = (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 104 | 28, 29, 15, 30, 31, 32, 103, 86, 88, 72 | evl1expd 22350 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))) ∈ 𝐵 ∧ ((𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))))) | 
| 105 | 104 | simprd 495 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘(𝑃𝐷(𝑋(+g‘𝑆)(𝐶‘((ℤRHom‘𝐾)‘𝐴)))))‘𝑦) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 106 | 95, 102, 105 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑃 ↑ 𝑦)(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 107 | 82, 106 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)) = (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴)))) | 
| 108 | 107 | eqcomd 2742 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ (𝑦(+g‘𝐾)((ℤRHom‘𝐾)‘𝐴))) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))) | 
| 109 | 63, 108 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))) | 
| 110 | 109 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))) | 
| 111 | 110 | ex 412 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝐾) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))) | 
| 112 | 111 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝐾) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))))) | 
| 113 | 22, 112 | mpdd 43 | . . . 4
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))) | 
| 114 | 113 | imp 406 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))) | 
| 115 | 114 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦))) | 
| 116 |  | aks6d1c1p2.1 | . . 3
⊢  ∼ =
{〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} | 
| 117 | 29 | ply1crng 22201 | . . . . . . . . 9
⊢ (𝐾 ∈ CRing → 𝑆 ∈ CRing) | 
| 118 | 4, 117 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 119 |  | crngring 20243 | . . . . . . . 8
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) | 
| 120 | 118, 119 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 121 | 120 | ringgrpd 20240 | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ Grp) | 
| 122 | 41, 35 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 123 | 121, 122,
52 | 3jca 1128 | . . . . 5
⊢ (𝜑 → (𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵)) | 
| 124 | 30, 58 | grpcl 18960 | . . . . 5
⊢ ((𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐶‘((ℤRHom‘𝐾)‘𝐴)) ∈ 𝐵) → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵) | 
| 125 | 123, 124 | syl 17 | . . . 4
⊢ (𝜑 → (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵) | 
| 126 | 23 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐹 = (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴)))) | 
| 127 | 126 | eleq1d 2825 | . . . 4
⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ (𝑋 + (𝐶‘((ℤRHom‘𝐾)‘𝐴))) ∈ 𝐵)) | 
| 128 | 125, 127 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝐵) | 
| 129 | 116, 128,
70 | aks6d1c1p1 42109 | . 2
⊢ (𝜑 → (𝑃 ∼ 𝐹 ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑃 ↑ ((𝑂‘𝐹)‘𝑦)) = ((𝑂‘𝐹)‘(𝑃 ↑ 𝑦)))) | 
| 130 | 115, 129 | mpbird 257 | 1
⊢ (𝜑 → 𝑃 ∼ 𝐹) |