| Step | Hyp | Ref
| Expression |
| 1 | | aks6d1c1p6.2 |
. 2
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
| 2 | | oveq1 7438 |
. . . 4
⊢ (ℎ = 0 → (ℎ𝐷𝐹) = (0𝐷𝐹)) |
| 3 | 2 | breq2d 5155 |
. . 3
⊢ (ℎ = 0 → (𝐸 ∼ (ℎ𝐷𝐹) ↔ 𝐸 ∼ (0𝐷𝐹))) |
| 4 | | oveq1 7438 |
. . . 4
⊢ (ℎ = 𝑖 → (ℎ𝐷𝐹) = (𝑖𝐷𝐹)) |
| 5 | 4 | breq2d 5155 |
. . 3
⊢ (ℎ = 𝑖 → (𝐸 ∼ (ℎ𝐷𝐹) ↔ 𝐸 ∼ (𝑖𝐷𝐹))) |
| 6 | | oveq1 7438 |
. . . 4
⊢ (ℎ = (𝑖 + 1) → (ℎ𝐷𝐹) = ((𝑖 + 1)𝐷𝐹)) |
| 7 | 6 | breq2d 5155 |
. . 3
⊢ (ℎ = (𝑖 + 1) → (𝐸 ∼ (ℎ𝐷𝐹) ↔ 𝐸 ∼ ((𝑖 + 1)𝐷𝐹))) |
| 8 | | oveq1 7438 |
. . . 4
⊢ (ℎ = 𝐿 → (ℎ𝐷𝐹) = (𝐿𝐷𝐹)) |
| 9 | 8 | breq2d 5155 |
. . 3
⊢ (ℎ = 𝐿 → (𝐸 ∼ (ℎ𝐷𝐹) ↔ 𝐸 ∼ (𝐿𝐷𝐹))) |
| 10 | | aks6d1c1.1 |
. . . . . . . . . . . . . . . 16
⊢ ∼ =
{〈𝑒, 𝑓〉 ∣ (𝑒 ∈ ℕ ∧ 𝑓 ∈ 𝐵 ∧ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝑒 ↑ ((𝑂‘𝑓)‘𝑦)) = ((𝑂‘𝑓)‘(𝑒 ↑ 𝑦)))} |
| 11 | | aks6d1c1p6.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸 ∼ 𝐹) |
| 12 | 10, 11 | aks6d1c1p1rcl 42109 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∈ ℕ ∧ 𝐹 ∈ 𝐵)) |
| 13 | 12 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
| 14 | | aks6d1c1.3 |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝑆) |
| 15 | 13, 14 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆)) |
| 16 | | aks6d1c1.5 |
. . . . . . . . . . . . . 14
⊢ 𝑊 = (mulGrp‘𝑆) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 18 | 16, 17 | mgpbas 20142 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑆) =
(Base‘𝑊) |
| 19 | 15, 18 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (Base‘𝑊)) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 21 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 22 | | aks6d1c1.9 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (.g‘𝑊) |
| 23 | 20, 21, 22 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Base‘𝑊) → (0𝐷𝐹) = (0g‘𝑊)) |
| 24 | 19, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0𝐷𝐹) = (0g‘𝑊)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑆) = (1r‘𝑆) |
| 26 | 16, 25 | ringidval 20180 |
. . . . . . . . . . . 12
⊢
(1r‘𝑆) = (0g‘𝑊) |
| 27 | 26 | eqcomi 2746 |
. . . . . . . . . . 11
⊢
(0g‘𝑊) = (1r‘𝑆) |
| 28 | 24, 27 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝜑 → (0𝐷𝐹) = (1r‘𝑆)) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (0𝐷𝐹) = (1r‘𝑆)) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑂‘(0𝐷𝐹)) = (𝑂‘(1r‘𝑆))) |
| 31 | 30 | fveq1d 6908 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(0𝐷𝐹))‘𝑦) = ((𝑂‘(1r‘𝑆))‘𝑦)) |
| 32 | 31 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(0𝐷𝐹))‘𝑦)) = (𝐸 ↑ ((𝑂‘(1r‘𝑆))‘𝑦))) |
| 33 | | aks6d1c1.13 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ Field) |
| 34 | 33 | fldcrngd 20742 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ CRing) |
| 35 | | crngring 20242 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Ring) |
| 37 | | aks6d1c1.2 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = (Poly1‘𝐾) |
| 38 | | aks6d1c1.8 |
. . . . . . . . . . . . . 14
⊢ 𝐶 = (algSc‘𝑆) |
| 39 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(1r‘𝐾) = (1r‘𝐾) |
| 40 | 37, 38, 39, 25 | ply1scl1 22296 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring → (𝐶‘(1r‘𝐾)) = (1r‘𝑆)) |
| 41 | 36, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶‘(1r‘𝐾)) = (1r‘𝑆)) |
| 42 | 41 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐶‘(1r‘𝐾)) = (1r‘𝑆)) |
| 43 | 42 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (1r‘𝑆) = (𝐶‘(1r‘𝐾))) |
| 44 | 43 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑂‘(1r‘𝑆)) = (𝑂‘(𝐶‘(1r‘𝐾)))) |
| 45 | 44 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(1r‘𝑆))‘𝑦) = ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦)) |
| 46 | 45 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(1r‘𝑆))‘𝑦)) = (𝐸 ↑ ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦))) |
| 47 | | aks6d1c1.11 |
. . . . . . . . . . 11
⊢ 𝑂 = (eval1‘𝐾) |
| 48 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 49 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐾 ∈ CRing) |
| 50 | 48, 39 | ringidcl 20262 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Ring →
(1r‘𝐾)
∈ (Base‘𝐾)) |
| 51 | 36, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾)) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (1r‘𝐾) ∈ (Base‘𝐾)) |
| 53 | | aks6d1c1.6 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑉 = (mulGrp‘𝐾) |
| 54 | 53 | crngmgp 20238 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ CRing → 𝑉 ∈ CMnd) |
| 55 | 34, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉 ∈ CMnd) |
| 56 | | aks6d1c1.15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 57 | 56 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
| 58 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(.g‘𝑉) = (.g‘𝑉) |
| 59 | 55, 57, 58 | isprimroot 42094 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) ↔ (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(.g‘𝑉)𝑦) = (0g‘𝑉) ∧ ∀𝑧 ∈ ℕ0 ((𝑧(.g‘𝑉)𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑧)))) |
| 60 | 59 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑉 PrimRoots 𝑅) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(.g‘𝑉)𝑦) = (0g‘𝑉) ∧ ∀𝑧 ∈ ℕ0 ((𝑧(.g‘𝑉)𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑧)))) |
| 61 | 60 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑦 ∈ (Base‘𝑉) ∧ (𝑅(.g‘𝑉)𝑦) = (0g‘𝑉) ∧ ∀𝑧 ∈ ℕ0 ((𝑧(.g‘𝑉)𝑦) = (0g‘𝑉) → 𝑅 ∥ 𝑧))) |
| 62 | 61 | simp1d 1143 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝑉)) |
| 63 | 53, 48 | mgpbas 20142 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐾) =
(Base‘𝑉) |
| 64 | 63 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢
(Base‘𝑉) =
(Base‘𝐾) |
| 65 | 62, 64 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑦 ∈ (Base‘𝐾)) |
| 66 | 47, 37, 48, 38, 14, 49, 52, 65 | evl1scad 22339 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐶‘(1r‘𝐾)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦) = (1r‘𝐾))) |
| 67 | 66 | simprd 495 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦) = (1r‘𝐾)) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦)) = (𝐸 ↑
(1r‘𝐾))) |
| 69 | 55 | cmnmndd 19822 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ Mnd) |
| 70 | 12 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℕ) |
| 71 | 70 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
| 72 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑉) =
(Base‘𝑉) |
| 73 | | aks6d1c1.7 |
. . . . . . . . . . 11
⊢ ↑ =
(.g‘𝑉) |
| 74 | 53, 39 | ringidval 20180 |
. . . . . . . . . . 11
⊢
(1r‘𝐾) = (0g‘𝑉) |
| 75 | 72, 73, 74 | mulgnn0z 19119 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Mnd ∧ 𝐸 ∈ ℕ0)
→ (𝐸 ↑
(1r‘𝐾)) =
(1r‘𝐾)) |
| 76 | 69, 71, 75 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ↑
(1r‘𝐾)) =
(1r‘𝐾)) |
| 77 | 76 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑
(1r‘𝐾)) =
(1r‘𝐾)) |
| 78 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝑉 ∈ Mnd) |
| 79 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → 𝐸 ∈
ℕ0) |
| 80 | 63, 73 | mulgnn0cl 19108 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ Mnd ∧ 𝐸 ∈ ℕ0
∧ 𝑦 ∈
(Base‘𝐾)) →
(𝐸 ↑ 𝑦) ∈ (Base‘𝐾)) |
| 81 | 78, 79, 65, 80 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ 𝑦) ∈ (Base‘𝐾)) |
| 82 | 47, 37, 48, 38, 14, 49, 52, 81 | evl1scad 22339 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝐶‘(1r‘𝐾)) ∈ 𝐵 ∧ ((𝑂‘(𝐶‘(1r‘𝐾)))‘(𝐸 ↑ 𝑦)) = (1r‘𝐾))) |
| 83 | 82 | simprd 495 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐶‘(1r‘𝐾)))‘(𝐸 ↑ 𝑦)) = (1r‘𝐾)) |
| 84 | 83 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (1r‘𝐾) = ((𝑂‘(𝐶‘(1r‘𝐾)))‘(𝐸 ↑ 𝑦))) |
| 85 | 68, 77, 84 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(𝐶‘(1r‘𝐾)))‘𝑦)) = ((𝑂‘(𝐶‘(1r‘𝐾)))‘(𝐸 ↑ 𝑦))) |
| 86 | 42 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑂‘(𝐶‘(1r‘𝐾))) = (𝑂‘(1r‘𝑆))) |
| 87 | 86 | fveq1d 6908 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(𝐶‘(1r‘𝐾)))‘(𝐸 ↑ 𝑦)) = ((𝑂‘(1r‘𝑆))‘(𝐸 ↑ 𝑦))) |
| 88 | 46, 85, 87 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(1r‘𝑆))‘𝑦)) = ((𝑂‘(1r‘𝑆))‘(𝐸 ↑ 𝑦))) |
| 89 | 29 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (1r‘𝑆) = (0𝐷𝐹)) |
| 90 | 89 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝑂‘(1r‘𝑆)) = (𝑂‘(0𝐷𝐹))) |
| 91 | 90 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → ((𝑂‘(1r‘𝑆))‘(𝐸 ↑ 𝑦)) = ((𝑂‘(0𝐷𝐹))‘(𝐸 ↑ 𝑦))) |
| 92 | 32, 88, 91 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑉 PrimRoots 𝑅)) → (𝐸 ↑ ((𝑂‘(0𝐷𝐹))‘𝑦)) = ((𝑂‘(0𝐷𝐹))‘(𝐸 ↑ 𝑦))) |
| 93 | 92 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘(0𝐷𝐹))‘𝑦)) = ((𝑂‘(0𝐷𝐹))‘(𝐸 ↑ 𝑦))) |
| 94 | 37 | ply1ring 22249 |
. . . . . . . 8
⊢ (𝐾 ∈ Ring → 𝑆 ∈ Ring) |
| 95 | 36, 94 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ Ring) |
| 96 | 17, 25 | ringidcl 20262 |
. . . . . . 7
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
| 97 | 95, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑆) ∈ (Base‘𝑆)) |
| 98 | 28 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → (1r‘𝑆) = (0𝐷𝐹)) |
| 99 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝑆)) |
| 100 | 99 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑆) = 𝐵) |
| 101 | 98, 100 | eleq12d 2835 |
. . . . . 6
⊢ (𝜑 →
((1r‘𝑆)
∈ (Base‘𝑆)
↔ (0𝐷𝐹) ∈ 𝐵)) |
| 102 | 97, 101 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (0𝐷𝐹) ∈ 𝐵) |
| 103 | 10, 102, 70 | aks6d1c1p1 42108 |
. . . 4
⊢ (𝜑 → (𝐸 ∼ (0𝐷𝐹) ↔ ∀𝑦 ∈ (𝑉 PrimRoots 𝑅)(𝐸 ↑ ((𝑂‘(0𝐷𝐹))‘𝑦)) = ((𝑂‘(0𝐷𝐹))‘(𝐸 ↑ 𝑦)))) |
| 104 | 93, 103 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐸 ∼ (0𝐷𝐹)) |
| 105 | | aks6d1c1.4 |
. . . . 5
⊢ 𝑋 = (var1‘𝐾) |
| 106 | | aks6d1c1.10 |
. . . . 5
⊢ 𝑃 = (chr‘𝐾) |
| 107 | | aks6d1c1.12 |
. . . . 5
⊢ + =
(+g‘𝑆) |
| 108 | 33 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐾 ∈ Field) |
| 109 | | aks6d1c1.14 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 110 | 109 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝑃 ∈ ℙ) |
| 111 | 56 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝑅 ∈ ℕ) |
| 112 | | aks6d1c1.18 |
. . . . . 6
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 113 | 112 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → (𝑁 gcd 𝑅) = 1) |
| 114 | | aks6d1c1.17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
| 115 | 114 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝑃 ∥ 𝑁) |
| 116 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐸 ∼ (𝑖𝐷𝐹)) |
| 117 | 11 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐸 ∼ 𝐹) |
| 118 | 10, 37, 14, 105, 16, 53, 73, 38, 22, 106, 47, 107, 108, 110, 111, 113, 115, 116, 117 | aks6d1c1p4 42112 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐸 ∼ ((𝑖𝐷𝐹)(+g‘𝑊)𝐹)) |
| 119 | 16 | ringmgp 20236 |
. . . . . . . 8
⊢ (𝑆 ∈ Ring → 𝑊 ∈ Mnd) |
| 120 | 95, 119 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ Mnd) |
| 121 | 120 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑊 ∈ Mnd) |
| 122 | 121 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝑊 ∈ Mnd) |
| 123 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝑖 ∈ ℕ0) |
| 124 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑆) = (Base‘𝑊)) |
| 125 | 99, 124 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = (Base‘𝑊)) |
| 126 | 125 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈ 𝐵 ↔ 𝐹 ∈ (Base‘𝑊))) |
| 127 | 13, 126 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (Base‘𝑊)) |
| 128 | 127 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐹 ∈ (Base‘𝑊)) |
| 129 | 128 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐹 ∈ (Base‘𝑊)) |
| 130 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 131 | 20, 22, 130 | mulgnn0p1 19103 |
. . . . 5
⊢ ((𝑊 ∈ Mnd ∧ 𝑖 ∈ ℕ0
∧ 𝐹 ∈
(Base‘𝑊)) →
((𝑖 + 1)𝐷𝐹) = ((𝑖𝐷𝐹)(+g‘𝑊)𝐹)) |
| 132 | 122, 123,
129, 131 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → ((𝑖 + 1)𝐷𝐹) = ((𝑖𝐷𝐹)(+g‘𝑊)𝐹)) |
| 133 | 118, 132 | breqtrrd 5171 |
. . 3
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝐸 ∼ (𝑖𝐷𝐹)) → 𝐸 ∼ ((𝑖 + 1)𝐷𝐹)) |
| 134 | 3, 5, 7, 9, 104, 133 | nn0indd 12715 |
. 2
⊢ ((𝜑 ∧ 𝐿 ∈ ℕ0) → 𝐸 ∼ (𝐿𝐷𝐹)) |
| 135 | 1, 134 | mpdan 687 |
1
⊢ (𝜑 → 𝐸 ∼ (𝐿𝐷𝐹)) |