| Step | Hyp | Ref
| Expression |
| 1 | | cnvimass 6100 |
. . . 4
⊢ (◡𝑂 “ ℕ) ⊆ dom 𝑂 |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 3 | | torsubg.1 |
. . . . . 6
⊢ 𝑂 = (od‘𝐺) |
| 4 | 2, 3 | odf 19555 |
. . . . 5
⊢ 𝑂:(Base‘𝐺)⟶ℕ0 |
| 5 | 4 | fdmi 6747 |
. . . 4
⊢ dom 𝑂 = (Base‘𝐺) |
| 6 | 1, 5 | sseqtri 4032 |
. . 3
⊢ (◡𝑂 “ ℕ) ⊆ (Base‘𝐺) |
| 7 | 6 | a1i 11 |
. 2
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ⊆ (Base‘𝐺)) |
| 8 | | ablgrp 19803 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 9 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 10 | 2, 9 | grpidcl 18983 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 11 | 8, 10 | syl 17 |
. . . 4
⊢ (𝐺 ∈ Abel →
(0g‘𝐺)
∈ (Base‘𝐺)) |
| 12 | 3, 9 | od1 19577 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑂‘(0g‘𝐺)) = 1) |
| 13 | 8, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ Abel → (𝑂‘(0g‘𝐺)) = 1) |
| 14 | | 1nn 12277 |
. . . . 5
⊢ 1 ∈
ℕ |
| 15 | 13, 14 | eqeltrdi 2849 |
. . . 4
⊢ (𝐺 ∈ Abel → (𝑂‘(0g‘𝐺)) ∈
ℕ) |
| 16 | | ffn 6736 |
. . . . . 6
⊢ (𝑂:(Base‘𝐺)⟶ℕ0 → 𝑂 Fn (Base‘𝐺)) |
| 17 | 4, 16 | ax-mp 5 |
. . . . 5
⊢ 𝑂 Fn (Base‘𝐺) |
| 18 | | elpreima 7078 |
. . . . 5
⊢ (𝑂 Fn (Base‘𝐺) →
((0g‘𝐺)
∈ (◡𝑂 “ ℕ) ↔
((0g‘𝐺)
∈ (Base‘𝐺) ∧
(𝑂‘(0g‘𝐺)) ∈
ℕ))) |
| 19 | 17, 18 | ax-mp 5 |
. . . 4
⊢
((0g‘𝐺) ∈ (◡𝑂 “ ℕ) ↔
((0g‘𝐺)
∈ (Base‘𝐺) ∧
(𝑂‘(0g‘𝐺)) ∈
ℕ)) |
| 20 | 11, 15, 19 | sylanbrc 583 |
. . 3
⊢ (𝐺 ∈ Abel →
(0g‘𝐺)
∈ (◡𝑂 “ ℕ)) |
| 21 | 20 | ne0d 4342 |
. 2
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ≠
∅) |
| 22 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝐺 ∈ Grp) |
| 23 | 6 | sseli 3979 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) → 𝑥 ∈ (Base‘𝐺)) |
| 24 | 23 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝑥 ∈ (Base‘𝐺)) |
| 25 | 6 | sseli 3979 |
. . . . . . . 8
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) → 𝑦 ∈ (Base‘𝐺)) |
| 26 | 25 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝑦 ∈ (Base‘𝐺)) |
| 27 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 28 | 2, 27 | grpcl 18959 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
| 29 | 22, 24, 26, 28 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
| 30 | | 0nnn 12302 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℕ |
| 31 | 2, 3 | odcl 19554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (Base‘𝐺) → (𝑂‘𝑥) ∈
ℕ0) |
| 32 | 24, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈
ℕ0) |
| 33 | 32 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℤ) |
| 34 | 2, 3 | odcl 19554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (Base‘𝐺) → (𝑂‘𝑦) ∈
ℕ0) |
| 35 | 26, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈
ℕ0) |
| 36 | 35 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈ ℤ) |
| 37 | 33, 36 | gcdcld 16545 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) gcd (𝑂‘𝑦)) ∈
ℕ0) |
| 38 | 37 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) gcd (𝑂‘𝑦)) ∈ ℂ) |
| 39 | 38 | mul02d 11459 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) = 0) |
| 40 | 39 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ 0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
| 41 | 33, 36 | zmulcld 12728 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℤ) |
| 42 | | 0dvds 16314 |
. . . . . . . . . . . 12
⊢ (((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℤ → (0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
| 44 | 40, 43 | bitrd 279 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
| 45 | | elpreima 7078 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 Fn (Base‘𝐺) → (𝑥 ∈ (◡𝑂 “ ℕ) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝑂‘𝑥) ∈ ℕ))) |
| 46 | 17, 45 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝑂‘𝑥) ∈ ℕ)) |
| 47 | 46 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) → (𝑂‘𝑥) ∈ ℕ) |
| 48 | 47 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℕ) |
| 49 | | elpreima 7078 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 Fn (Base‘𝐺) → (𝑦 ∈ (◡𝑂 “ ℕ) ↔ (𝑦 ∈ (Base‘𝐺) ∧ (𝑂‘𝑦) ∈ ℕ))) |
| 50 | 17, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) ↔ (𝑦 ∈ (Base‘𝐺) ∧ (𝑂‘𝑦) ∈ ℕ)) |
| 51 | 50 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) → (𝑂‘𝑦) ∈ ℕ) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈ ℕ) |
| 53 | 48, 52 | nnmulcld 12319 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℕ) |
| 54 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (((𝑂‘𝑥) · (𝑂‘𝑦)) = 0 → (((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℕ ↔ 0 ∈
ℕ)) |
| 55 | 53, 54 | syl5ibcom 245 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (((𝑂‘𝑥) · (𝑂‘𝑦)) = 0 → 0 ∈
ℕ)) |
| 56 | 44, 55 | sylbid 240 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) → 0 ∈ ℕ)) |
| 57 | 30, 56 | mtoi 199 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ¬ (0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
| 58 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝐺 ∈ Abel) |
| 59 | 3, 2, 27 | odadd1 19866 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
| 60 | 58, 24, 26, 59 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
| 61 | | oveq1 7438 |
. . . . . . . . . 10
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) = (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦)))) |
| 62 | 61 | breq1d 5153 |
. . . . . . . . 9
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → (((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
| 63 | 60, 62 | syl5ibcom 245 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
| 64 | 57, 63 | mtod 198 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ¬ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0) |
| 65 | 2, 3 | odcl 19554 |
. . . . . . . . . 10
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈
ℕ0) |
| 66 | 29, 65 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈
ℕ0) |
| 67 | | elnn0 12528 |
. . . . . . . . 9
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ0 ↔ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ ∨ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
| 68 | 66, 67 | sylib 218 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ ∨ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
| 69 | 68 | ord 865 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (¬ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ → (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
| 70 | 64, 69 | mt3d 148 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ) |
| 71 | | elpreima 7078 |
. . . . . . 7
⊢ (𝑂 Fn (Base‘𝐺) → ((𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ↔ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ))) |
| 72 | 17, 71 | ax-mp 5 |
. . . . . 6
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ↔ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ)) |
| 73 | 29, 70, 72 | sylanbrc 583 |
. . . . 5
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ)) |
| 74 | 73 | ralrimiva 3146 |
. . . 4
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → ∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ)) |
| 75 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 76 | 2, 75 | grpinvcl 19005 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺)) |
| 77 | 8, 23, 76 | syl2an 596 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) →
((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺)) |
| 78 | 3, 75, 2 | odinv 19579 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑂‘((invg‘𝐺)‘𝑥)) = (𝑂‘𝑥)) |
| 79 | 8, 23, 78 | syl2an 596 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘((invg‘𝐺)‘𝑥)) = (𝑂‘𝑥)) |
| 80 | 47 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℕ) |
| 81 | 79, 80 | eqeltrd 2841 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ) |
| 82 | | elpreima 7078 |
. . . . . 6
⊢ (𝑂 Fn (Base‘𝐺) →
(((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ) ↔
(((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺) ∧ (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ))) |
| 83 | 17, 82 | ax-mp 5 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ) ↔
(((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺) ∧ (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ)) |
| 84 | 77, 81, 83 | sylanbrc 583 |
. . . 4
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) →
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ)) |
| 85 | 74, 84 | jca 511 |
. . 3
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))) |
| 86 | 85 | ralrimiva 3146 |
. 2
⊢ (𝐺 ∈ Abel →
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))) |
| 87 | 2, 27, 75 | issubg2 19159 |
. . 3
⊢ (𝐺 ∈ Grp → ((◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺) ↔ ((◡𝑂 “ ℕ) ⊆ (Base‘𝐺) ∧ (◡𝑂 “ ℕ) ≠ ∅ ∧
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))))) |
| 88 | 8, 87 | syl 17 |
. 2
⊢ (𝐺 ∈ Abel → ((◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺) ↔ ((◡𝑂 “ ℕ) ⊆ (Base‘𝐺) ∧ (◡𝑂 “ ℕ) ≠ ∅ ∧
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))))) |
| 89 | 7, 21, 86, 88 | mpbir3and 1343 |
1
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺)) |