| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(𝑅
↾s 𝑈)) =
(Base‘(𝑅
↾s 𝑈)) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(.g‘(𝑅 ↾s 𝑈)) = (.g‘(𝑅 ↾s 𝑈)) |
| 3 | | primrootscoprmpow.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 4 | | primrootscoprmpow.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 5 | | primrootscoprmpow.6 |
. . . . . . . . . 10
⊢ 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} |
| 6 | 3, 4, 5 | primrootsunit 42099 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ∧ (𝑅 ↾s 𝑈) ∈ Abel)) |
| 7 | 6 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Abel) |
| 8 | 7 | ablcmnd 19806 |
. . . . . . 7
⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ CMnd) |
| 9 | 8 | cmnmndd 19822 |
. . . . . 6
⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Mnd) |
| 10 | | primrootscoprmpow.3 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℕ) |
| 11 | 10 | nnnn0d 12587 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
| 12 | | primrootscoprmpow.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (𝑅 PrimRoots 𝐾)) |
| 13 | 6 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) |
| 14 | 13 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑀 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))) |
| 15 | 12, 14 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) |
| 16 | 4 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 17 | 8, 16, 2 | isprimroot 42094 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))) |
| 18 | 17 | biimpd 229 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) → (𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))) |
| 19 | 15, 18 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))) |
| 20 | 19 | simp1d 1143 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 21 | 1, 2, 9, 11, 20 | mulgnn0cld 19113 |
. . . . 5
⊢ (𝜑 → (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 22 | 5 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ 𝑈 ↔ 𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) |
| 23 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑐 → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)𝑐)) |
| 24 | 23 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑐 → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))) |
| 25 | 24 | rexbidv 3179 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑐 → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))) |
| 26 | 25 | elrab 3692 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)} ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))) |
| 27 | 22, 26 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝑈 ↔ (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))) |
| 28 | 27 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ 𝑈 → (𝑐 ∈ (Base‘𝑅) ∧ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑐) = (0g‘𝑅))) |
| 29 | 28 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅)) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑈) → 𝑐 ∈ (Base‘𝑅)) |
| 31 | 30 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑐 ∈ 𝑈 → 𝑐 ∈ (Base‘𝑅))) |
| 32 | 31 | ssrdv 3989 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ (Base‘𝑅)) |
| 33 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (0g‘𝑅) → (𝑖(+g‘𝑅)𝑎) = (𝑖(+g‘𝑅)(0g‘𝑅))) |
| 34 | 33 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑎 = (0g‘𝑅) → ((𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ (𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))) |
| 35 | 34 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑎 = (0g‘𝑅) → (∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅) ↔ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))) |
| 36 | 3 | cmnmndd 19822 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 39 | 37, 38 | mndidcl 18762 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ (Base‘𝑅)) |
| 40 | 36, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
| 41 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → 𝑖 = (0g‘𝑅)) |
| 42 | 41 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → (𝑖(+g‘𝑅)(0g‘𝑅)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅))) |
| 43 | 42 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (0g‘𝑅)) → ((𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))) |
| 44 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 45 | 37, 44, 38 | mndlid 18767 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Mnd ∧
(0g‘𝑅)
∈ (Base‘𝑅))
→ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 46 | 36, 40, 45 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 47 | 40, 43, 46 | rspcedvd 3624 |
. . . . . . . . . . 11
⊢ (𝜑 → ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 48 | 35, 40, 47 | elrabd 3694 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑅) ∈ {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) |
| 49 | 5 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)}) |
| 50 | 49 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝜑 →
((0g‘𝑅)
∈ 𝑈 ↔
(0g‘𝑅)
∈ {𝑎 ∈
(Base‘𝑅) ∣
∃𝑖 ∈
(Base‘𝑅)(𝑖(+g‘𝑅)𝑎) = (0g‘𝑅)})) |
| 51 | 48, 50 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑅) ∈ 𝑈) |
| 52 | 32, 51, 9 | 3jca 1129 |
. . . . . . . 8
⊢ (𝜑 → (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈 ∧ (𝑅 ↾s 𝑈) ∈ Mnd)) |
| 53 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑅 ↾s 𝑈) = (𝑅 ↾s 𝑈) |
| 54 | 37, 38, 53 | issubm2 18817 |
. . . . . . . . 9
⊢ (𝑅 ∈ Mnd → (𝑈 ∈ (SubMnd‘𝑅) ↔ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈 ∧ (𝑅 ↾s 𝑈) ∈ Mnd))) |
| 55 | 36, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑈 ∈ (SubMnd‘𝑅) ↔ (𝑈 ⊆ (Base‘𝑅) ∧ (0g‘𝑅) ∈ 𝑈 ∧ (𝑅 ↾s 𝑈) ∈ Mnd))) |
| 56 | 52, 55 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ (SubMnd‘𝑅)) |
| 57 | 53, 37 | ressbas2 17283 |
. . . . . . . . . 10
⊢ (𝑈 ⊆ (Base‘𝑅) → 𝑈 = (Base‘(𝑅 ↾s 𝑈))) |
| 58 | 32, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 = (Base‘(𝑅 ↾s 𝑈))) |
| 59 | 58 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∈ 𝑈 ↔ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 60 | 20, 59 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝑈) |
| 61 | | eqid 2737 |
. . . . . . . 8
⊢
(.g‘𝑅) = (.g‘𝑅) |
| 62 | 61, 53, 2 | submmulg 19136 |
. . . . . . 7
⊢ ((𝑈 ∈ (SubMnd‘𝑅) ∧ 𝐸 ∈ ℕ0 ∧ 𝑀 ∈ 𝑈) → (𝐸(.g‘𝑅)𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 63 | 56, 11, 60, 62 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 64 | 63 | eleq1d 2826 |
. . . . 5
⊢ (𝜑 → ((𝐸(.g‘𝑅)𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)) ↔ (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 65 | 21, 64 | mpbird 257 |
. . . 4
⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 66 | 63 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 67 | 7 | ablgrpd 19804 |
. . . . . . 7
⊢ (𝜑 → (𝑅 ↾s 𝑈) ∈ Grp) |
| 68 | 16 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 69 | 11 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℤ) |
| 70 | 68, 69, 20 | 3jca 1129 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐸 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 71 | 1, 2 | mulgass 19129 |
. . . . . . 7
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝐾 ∈ ℤ ∧ 𝐸 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝐾 · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 72 | 67, 70, 71 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝐾 · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 73 | 4 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 74 | 10 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 75 | 73, 74 | mulcomd 11282 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 · 𝐸) = (𝐸 · 𝐾)) |
| 76 | 75 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((𝐾 · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((𝐸 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 77 | 69, 68, 20 | 3jca 1129 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 78 | 1, 2 | mulgass 19129 |
. . . . . . . . 9
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝐸 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝐸 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 79 | 67, 77, 78 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 80 | 19 | simp2d 1144 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 81 | 80 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀)) = (𝐸(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈)))) |
| 82 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘(𝑅 ↾s 𝑈)) = (0g‘(𝑅 ↾s 𝑈)) |
| 83 | 1, 2, 82 | mulgz 19120 |
. . . . . . . . . 10
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝐸 ∈ ℤ) → (𝐸(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) =
(0g‘(𝑅
↾s 𝑈))) |
| 84 | 67, 69, 83 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈))) |
| 85 | 81, 84 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (𝐸(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 86 | 79, 85 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((𝐸 · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 87 | 76, 86 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝐾 · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 88 | 72, 87 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 89 | 66, 88 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 90 | 19 | simp3d 1145 |
. . . . 5
⊢ (𝜑 → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) |
| 91 | | simp-6r 788 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 𝑙 ∈ ℕ0) |
| 92 | 91 | nn0cnd 12589 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 𝑙 ∈ ℂ) |
| 93 | 92 | mullidd 11279 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (1 · 𝑙) = 𝑙) |
| 94 | 93 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 𝑙 = (1 · 𝑙)) |
| 95 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) |
| 96 | | primrootscoprmpow.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 gcd 𝐾) = 1) |
| 97 | 96 | ad6antr 736 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (𝐸 gcd 𝐾) = 1) |
| 98 | 95, 97 | eqtr3d 2779 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → ((𝐸 · 𝑥) + (𝐾 · 𝑦)) = 1) |
| 99 | 95, 98 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 1 = (𝐸 gcd 𝐾)) |
| 100 | 99 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (1 · 𝑙) = ((𝐸 gcd 𝐾) · 𝑙)) |
| 101 | 94, 100 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 𝑙 = ((𝐸 gcd 𝐾) · 𝑙)) |
| 102 | 101 | oveq1d 7446 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (((𝐸 gcd 𝐾) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 103 | 95 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → ((𝐸 gcd 𝐾) · 𝑙) = (((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)) |
| 104 | 103 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (((𝐸 gcd 𝐾) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 105 | | simp-4l 783 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝜑 ∧ 𝑙 ∈
ℕ0)) |
| 106 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 107 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 108 | 105, 106,
107 | jca31 514 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ)) |
| 109 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ) |
| 110 | 108, 109 | jca 511 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ)) |
| 111 | 74 | ad4antr 732 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝐸 ∈ ℂ) |
| 112 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 113 | 112 | zcnd 12723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑥 ∈ ℂ) |
| 114 | 111, 113 | mulcld 11281 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝐸 · 𝑥) ∈ ℂ) |
| 115 | 73 | ad4antr 732 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝐾 ∈ ℂ) |
| 116 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℤ) |
| 117 | 116 | zcnd 12723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈ ℂ) |
| 118 | 115, 117 | mulcld 11281 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝐾 · 𝑦) ∈ ℂ) |
| 119 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈ ℕ0) |
| 120 | 119 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈ ℂ) |
| 121 | 114, 118,
120 | adddird 11286 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙) = (((𝐸 · 𝑥) · 𝑙) + ((𝐾 · 𝑦) · 𝑙))) |
| 122 | 121 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((((𝐸 · 𝑥) · 𝑙) + ((𝐾 · 𝑦) · 𝑙))(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 123 | 67 | ad4antr 732 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝑅 ↾s 𝑈) ∈ Grp) |
| 124 | 69 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝐸 ∈ ℤ) |
| 125 | 124, 112 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝐸 · 𝑥) ∈ ℤ) |
| 126 | 119 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈ ℤ) |
| 127 | 125, 126 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((𝐸 · 𝑥) · 𝑙) ∈ ℤ) |
| 128 | 68 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝐾 ∈ ℤ) |
| 129 | 128, 116 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝐾 · 𝑦) ∈ ℤ) |
| 130 | 129, 126 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((𝐾 · 𝑦) · 𝑙) ∈ ℤ) |
| 131 | 20 | ad4antr 732 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 132 | 127, 130,
131 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (((𝐸 · 𝑥) · 𝑙) ∈ ℤ ∧ ((𝐾 · 𝑦) · 𝑙) ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 133 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘(𝑅 ↾s 𝑈)) = (+g‘(𝑅 ↾s 𝑈)) |
| 134 | 1, 2, 133 | mulgdir 19124 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (((𝐸 · 𝑥) · 𝑙) ∈ ℤ ∧ ((𝐾 · 𝑦) · 𝑙) ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((((𝐸 · 𝑥) · 𝑙) + ((𝐾 · 𝑦) · 𝑙))(.g‘(𝑅 ↾s 𝑈))𝑀) = ((((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)(+g‘(𝑅 ↾s 𝑈))(((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 135 | 123, 132,
134 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) · 𝑙) + ((𝐾 · 𝑦) · 𝑙))(.g‘(𝑅 ↾s 𝑈))𝑀) = ((((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)(+g‘(𝑅 ↾s 𝑈))(((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 136 | 74 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℂ) |
| 137 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 138 | 137 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ) |
| 139 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑙 ∈ ℕ0) |
| 140 | 139 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑙 ∈ ℂ) |
| 141 | 136, 138,
140 | mulassd 11284 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → ((𝐸 · 𝑥) · 𝑙) = (𝐸 · (𝑥 · 𝑙))) |
| 142 | 138, 140 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝑙) ∈ ℂ) |
| 143 | 136, 142 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝐸 · (𝑥 · 𝑙)) = ((𝑥 · 𝑙) · 𝐸)) |
| 144 | 141, 143 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → ((𝐸 · 𝑥) · 𝑙) = ((𝑥 · 𝑙) · 𝐸)) |
| 145 | 144 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (((𝑥 · 𝑙) · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 146 | 67 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑅 ↾s 𝑈) ∈ Grp) |
| 147 | 139 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑙 ∈ ℤ) |
| 148 | 137, 147 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥 · 𝑙) ∈ ℤ) |
| 149 | 69 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℤ) |
| 150 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 151 | 148, 149,
150 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑙) ∈ ℤ ∧ 𝐸 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 152 | 1, 2 | mulgass 19129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ ((𝑥 · 𝑙) ∈ ℤ ∧ 𝐸 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) → (((𝑥 · 𝑙) · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((𝑥 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 153 | 146, 151,
152 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑙) · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((𝑥 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 154 | 21 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 155 | 137, 147,
154 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 156 | 1, 2 | mulgass 19129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑥 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)))) → ((𝑥 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (𝑥(.g‘(𝑅 ↾s 𝑈))(𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)))) |
| 157 | 146, 155,
156 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (𝑥(.g‘(𝑅 ↾s 𝑈))(𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)))) |
| 158 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ0) → 𝑈 ∈ (SubMnd‘𝑅)) |
| 159 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ0) → 𝐸 ∈
ℕ0) |
| 160 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ0) → 𝑀 ∈ 𝑈) |
| 161 | 158, 159,
160, 62 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ0) → (𝐸(.g‘𝑅)𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 162 | 161 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝐸(.g‘𝑅)𝑀) = (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 163 | 162 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝐸(.g‘(𝑅 ↾s 𝑈))𝑀) = (𝐸(.g‘𝑅)𝑀)) |
| 164 | 163 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀))) |
| 165 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 166 | 164, 165 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 167 | 166 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥(.g‘(𝑅 ↾s 𝑈))(𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) = (𝑥(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈)))) |
| 168 | 1, 2, 82 | mulgz 19120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ 𝑥 ∈ ℤ) → (𝑥(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) =
(0g‘(𝑅
↾s 𝑈))) |
| 169 | 146, 137,
168 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈))) |
| 170 | 167, 169 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (𝑥(.g‘(𝑅 ↾s 𝑈))(𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀))) = (0g‘(𝑅 ↾s 𝑈))) |
| 171 | 157, 170 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 172 | 153, 171 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (((𝑥 · 𝑙) · 𝐸)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 173 | 145, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) → (((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 174 | 173 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 175 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (𝜑 ∧ 𝑙 ∈
ℕ0)) |
| 176 | 175, 116 | jca 511 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈
ℤ)) |
| 177 | 73 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝐾 ∈
ℂ) |
| 178 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℤ) |
| 179 | 178 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑦 ∈
ℂ) |
| 180 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈
ℕ0) |
| 181 | 180 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈
ℂ) |
| 182 | 177, 179,
181 | mulassd 11284 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝐾 · 𝑦) · 𝑙) = (𝐾 · (𝑦 · 𝑙))) |
| 183 | 179, 181 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (𝑦 · 𝑙) ∈ ℂ) |
| 184 | 177, 183 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (𝐾 · (𝑦 · 𝑙)) = ((𝑦 · 𝑙) · 𝐾)) |
| 185 | 182, 184 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝐾 · 𝑦) · 𝑙) = ((𝑦 · 𝑙) · 𝐾)) |
| 186 | 185 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (((𝑦 · 𝑙) · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀)) |
| 187 | 67 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (𝑅 ↾s 𝑈) ∈ Grp) |
| 188 | 180 | nn0zd 12639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑙 ∈
ℤ) |
| 189 | 178, 188 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (𝑦 · 𝑙) ∈ ℤ) |
| 190 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝐾 ∈
ℤ) |
| 191 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈))) |
| 192 | 189, 190,
191 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝑦 · 𝑙) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) |
| 193 | 1, 2 | mulgass 19129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ ((𝑦 · 𝑙) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅 ↾s 𝑈)))) → (((𝑦 · 𝑙) · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 194 | 187, 192,
193 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (((𝑦 · 𝑙) · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀))) |
| 195 | 80 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (𝐾(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 196 | 195 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀)) = ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈)))) |
| 197 | 1, 2, 82 | mulgz 19120 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ↾s 𝑈) ∈ Grp ∧ (𝑦 · 𝑙) ∈ ℤ) → ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈))) |
| 198 | 187, 189,
197 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈))) |
| 199 | 196, 198 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → ((𝑦 · 𝑙)(.g‘(𝑅 ↾s 𝑈))(𝐾(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 200 | 194, 199 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (((𝑦 · 𝑙) · 𝐾)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 201 | 186, 200 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ 𝑦 ∈ ℤ) → (((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 202 | 176, 201 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → (((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 203 | 174, 202 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)(+g‘(𝑅 ↾s 𝑈))(((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)) = ((0g‘(𝑅 ↾s 𝑈))(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈)))) |
| 204 | 1, 82 | grpidcl 18983 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ↾s 𝑈) ∈ Grp →
(0g‘(𝑅
↾s 𝑈))
∈ (Base‘(𝑅
↾s 𝑈))) |
| 205 | 123, 204 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) →
(0g‘(𝑅
↾s 𝑈))
∈ (Base‘(𝑅
↾s 𝑈))) |
| 206 | 1, 133, 82, 123, 205 | grpridd 18988 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) →
((0g‘(𝑅
↾s 𝑈))(+g‘(𝑅 ↾s 𝑈))(0g‘(𝑅 ↾s 𝑈))) = (0g‘(𝑅 ↾s 𝑈))) |
| 207 | 203, 206 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)(+g‘(𝑅 ↾s 𝑈))(((𝐾 · 𝑦) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀)) = (0g‘(𝑅 ↾s 𝑈))) |
| 208 | 135, 207 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) · 𝑙) + ((𝐾 · 𝑦) · 𝑙))(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 209 | 122, 208 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 210 | 110, 209 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) → ((((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 211 | 210 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → ((((𝐸 · 𝑥) + (𝐾 · 𝑦)) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 212 | 104, 211 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (((𝐸 gcd 𝐾) · 𝑙)(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 213 | 102, 212 | eqtrd 2777 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → (𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈))) |
| 214 | | simp-5r 786 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) |
| 215 | 213, 214 | mpd 15 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑙 ∈ ℕ0)
∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) ∧ 𝑥 ∈ ℤ) ∧ 𝑦 ∈ ℤ) ∧ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) → 𝐾 ∥ 𝑙) |
| 216 | | bezout 16580 |
. . . . . . . . . . 11
⊢ ((𝐸 ∈ ℤ ∧ 𝐾 ∈ ℤ) →
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℤ
(𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) |
| 217 | 69, 68, 216 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) |
| 218 | 217 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐸 gcd 𝐾) = ((𝐸 · 𝑥) + (𝐾 · 𝑦))) |
| 219 | 215, 218 | r19.29vva 3216 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) ∧ (𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈))) → 𝐾 ∥ 𝑙) |
| 220 | 219 | ex 412 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑙 ∈ ℕ0) ∧ ((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) → ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) |
| 221 | 220 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ ℕ0) → (((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) → ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))) |
| 222 | 221 | ralimdva 3167 |
. . . . 5
⊢ (𝜑 → (∀𝑙 ∈ ℕ0
((𝑙(.g‘(𝑅 ↾s 𝑈))𝑀) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙) → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))) |
| 223 | 90, 222 | mpd 15 |
. . . 4
⊢ (𝜑 → ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)) |
| 224 | 65, 89, 223 | 3jca 1129 |
. . 3
⊢ (𝜑 → ((𝐸(.g‘𝑅)𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙))) |
| 225 | | nnnn0 12533 |
. . . . 5
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
| 226 | 4, 225 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 227 | 8, 226, 2 | isprimroot 42094 |
. . 3
⊢ (𝜑 → ((𝐸(.g‘𝑅)𝑀) ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾) ↔ ((𝐸(.g‘𝑅)𝑀) ∈ (Base‘(𝑅 ↾s 𝑈)) ∧ (𝐾(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅 ↾s 𝑈))(𝐸(.g‘𝑅)𝑀)) = (0g‘(𝑅 ↾s 𝑈)) → 𝐾 ∥ 𝑙)))) |
| 228 | 224, 227 | mpbird 257 |
. 2
⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾)) |
| 229 | 13 | eleq2d 2827 |
. 2
⊢ (𝜑 → ((𝐸(.g‘𝑅)𝑀) ∈ (𝑅 PrimRoots 𝐾) ↔ (𝐸(.g‘𝑅)𝑀) ∈ ((𝑅 ↾s 𝑈) PrimRoots 𝐾))) |
| 230 | 228, 229 | mpbird 257 |
1
⊢ (𝜑 → (𝐸(.g‘𝑅)𝑀) ∈ (𝑅 PrimRoots 𝐾)) |