Step | Hyp | Ref
| Expression |
1 | | cnvimass 5404 |
. . . 4
⊢ (◡𝑂 “ ℕ) ⊆ dom 𝑂 |
2 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
3 | | torsubg.1 |
. . . . . 6
⊢ 𝑂 = (od‘𝐺) |
4 | 2, 3 | odf 17779 |
. . . . 5
⊢ 𝑂:(Base‘𝐺)⟶ℕ0 |
5 | 4 | fdmi 5965 |
. . . 4
⊢ dom 𝑂 = (Base‘𝐺) |
6 | 1, 5 | sseqtri 3600 |
. . 3
⊢ (◡𝑂 “ ℕ) ⊆ (Base‘𝐺) |
7 | 6 | a1i 11 |
. 2
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ⊆ (Base‘𝐺)) |
8 | | ablgrp 18021 |
. . . . 5
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
9 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
10 | 2, 9 | grpidcl 17273 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (Base‘𝐺)) |
11 | 8, 10 | syl 17 |
. . . 4
⊢ (𝐺 ∈ Abel →
(0g‘𝐺)
∈ (Base‘𝐺)) |
12 | 3, 9 | od1 17799 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑂‘(0g‘𝐺)) = 1) |
13 | 8, 12 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ Abel → (𝑂‘(0g‘𝐺)) = 1) |
14 | | 1nn 10908 |
. . . . 5
⊢ 1 ∈
ℕ |
15 | 13, 14 | syl6eqel 2696 |
. . . 4
⊢ (𝐺 ∈ Abel → (𝑂‘(0g‘𝐺)) ∈
ℕ) |
16 | | ffn 5958 |
. . . . . 6
⊢ (𝑂:(Base‘𝐺)⟶ℕ0 → 𝑂 Fn (Base‘𝐺)) |
17 | 4, 16 | ax-mp 5 |
. . . . 5
⊢ 𝑂 Fn (Base‘𝐺) |
18 | | elpreima 6245 |
. . . . 5
⊢ (𝑂 Fn (Base‘𝐺) →
((0g‘𝐺)
∈ (◡𝑂 “ ℕ) ↔
((0g‘𝐺)
∈ (Base‘𝐺) ∧
(𝑂‘(0g‘𝐺)) ∈
ℕ))) |
19 | 17, 18 | ax-mp 5 |
. . . 4
⊢
((0g‘𝐺) ∈ (◡𝑂 “ ℕ) ↔
((0g‘𝐺)
∈ (Base‘𝐺) ∧
(𝑂‘(0g‘𝐺)) ∈
ℕ)) |
20 | 11, 15, 19 | sylanbrc 695 |
. . 3
⊢ (𝐺 ∈ Abel →
(0g‘𝐺)
∈ (◡𝑂 “ ℕ)) |
21 | | ne0i 3880 |
. . 3
⊢
((0g‘𝐺) ∈ (◡𝑂 “ ℕ) → (◡𝑂 “ ℕ) ≠
∅) |
22 | 20, 21 | syl 17 |
. 2
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ≠
∅) |
23 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝐺 ∈ Grp) |
24 | 6 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) → 𝑥 ∈ (Base‘𝐺)) |
25 | 24 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝑥 ∈ (Base‘𝐺)) |
26 | 6 | sseli 3564 |
. . . . . . . 8
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) → 𝑦 ∈ (Base‘𝐺)) |
27 | 26 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝑦 ∈ (Base‘𝐺)) |
28 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
29 | 2, 28 | grpcl 17253 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
30 | 23, 25, 27, 29 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
31 | | 0nnn 10929 |
. . . . . . . . 9
⊢ ¬ 0
∈ ℕ |
32 | 2, 3 | odcl 17778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (Base‘𝐺) → (𝑂‘𝑥) ∈
ℕ0) |
33 | 25, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈
ℕ0) |
34 | 33 | nn0zd 11356 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℤ) |
35 | 2, 3 | odcl 17778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (Base‘𝐺) → (𝑂‘𝑦) ∈
ℕ0) |
36 | 27, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈
ℕ0) |
37 | 36 | nn0zd 11356 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈ ℤ) |
38 | 34, 37 | gcdcld 15068 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) gcd (𝑂‘𝑦)) ∈
ℕ0) |
39 | 38 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) gcd (𝑂‘𝑦)) ∈ ℂ) |
40 | 39 | mul02d 10113 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) = 0) |
41 | 40 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ 0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
42 | 34, 37 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℤ) |
43 | | 0dvds 14840 |
. . . . . . . . . . . 12
⊢ (((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℤ → (0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (0 ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
45 | 41, 44 | bitrd 267 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ ((𝑂‘𝑥) · (𝑂‘𝑦)) = 0)) |
46 | | elpreima 6245 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 Fn (Base‘𝐺) → (𝑥 ∈ (◡𝑂 “ ℕ) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝑂‘𝑥) ∈ ℕ))) |
47 | 17, 46 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) ↔ (𝑥 ∈ (Base‘𝐺) ∧ (𝑂‘𝑥) ∈ ℕ)) |
48 | 47 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (◡𝑂 “ ℕ) → (𝑂‘𝑥) ∈ ℕ) |
49 | 48 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℕ) |
50 | | elpreima 6245 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 Fn (Base‘𝐺) → (𝑦 ∈ (◡𝑂 “ ℕ) ↔ (𝑦 ∈ (Base‘𝐺) ∧ (𝑂‘𝑦) ∈ ℕ))) |
51 | 17, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) ↔ (𝑦 ∈ (Base‘𝐺) ∧ (𝑂‘𝑦) ∈ ℕ)) |
52 | 51 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (◡𝑂 “ ℕ) → (𝑂‘𝑦) ∈ ℕ) |
53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑦) ∈ ℕ) |
54 | 49, 53 | nnmulcld 10945 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℕ) |
55 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (((𝑂‘𝑥) · (𝑂‘𝑦)) = 0 → (((𝑂‘𝑥) · (𝑂‘𝑦)) ∈ ℕ ↔ 0 ∈
ℕ)) |
56 | 54, 55 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (((𝑂‘𝑥) · (𝑂‘𝑦)) = 0 → 0 ∈
ℕ)) |
57 | 45, 56 | sylbid 229 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) → 0 ∈ ℕ)) |
58 | 31, 57 | mtoi 189 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ¬ (0 ·
((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
59 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → 𝐺 ∈ Abel) |
60 | 3, 2, 28 | odadd1 18074 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
61 | 59, 25, 27, 60 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦))) |
62 | | oveq1 6556 |
. . . . . . . . . 10
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) = (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦)))) |
63 | 62 | breq1d 4593 |
. . . . . . . . 9
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → (((𝑂‘(𝑥(+g‘𝐺)𝑦)) · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)) ↔ (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
64 | 61, 63 | syl5ibcom 234 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0 → (0 · ((𝑂‘𝑥) gcd (𝑂‘𝑦))) ∥ ((𝑂‘𝑥) · (𝑂‘𝑦)))) |
65 | 58, 64 | mtod 188 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ¬ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0) |
66 | 2, 3 | odcl 17778 |
. . . . . . . . . 10
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈
ℕ0) |
67 | 30, 66 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈
ℕ0) |
68 | | elnn0 11171 |
. . . . . . . . 9
⊢ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ0 ↔ ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ ∨ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
69 | 67, 68 | sylib 207 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → ((𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ ∨ (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
70 | 69 | ord 391 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (¬ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ → (𝑂‘(𝑥(+g‘𝐺)𝑦)) = 0)) |
71 | 65, 70 | mt3d 139 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ) |
72 | | elpreima 6245 |
. . . . . . 7
⊢ (𝑂 Fn (Base‘𝐺) → ((𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ↔ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ))) |
73 | 17, 72 | ax-mp 5 |
. . . . . 6
⊢ ((𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ↔ ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ (𝑂‘(𝑥(+g‘𝐺)𝑦)) ∈ ℕ)) |
74 | 30, 71, 73 | sylanbrc 695 |
. . . . 5
⊢ (((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) ∧ 𝑦 ∈ (◡𝑂 “ ℕ)) → (𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ)) |
75 | 74 | ralrimiva 2949 |
. . . 4
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → ∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ)) |
76 | | eqid 2610 |
. . . . . . 7
⊢
(invg‘𝐺) = (invg‘𝐺) |
77 | 2, 76 | grpinvcl 17290 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) →
((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺)) |
78 | 8, 24, 77 | syl2an 493 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) →
((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺)) |
79 | 3, 76, 2 | odinv 17801 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐺)) → (𝑂‘((invg‘𝐺)‘𝑥)) = (𝑂‘𝑥)) |
80 | 8, 24, 79 | syl2an 493 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘((invg‘𝐺)‘𝑥)) = (𝑂‘𝑥)) |
81 | 48 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘𝑥) ∈ ℕ) |
82 | 80, 81 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ) |
83 | | elpreima 6245 |
. . . . . 6
⊢ (𝑂 Fn (Base‘𝐺) →
(((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ) ↔
(((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺) ∧ (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ))) |
84 | 17, 83 | ax-mp 5 |
. . . . 5
⊢
(((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ) ↔
(((invg‘𝐺)‘𝑥) ∈ (Base‘𝐺) ∧ (𝑂‘((invg‘𝐺)‘𝑥)) ∈ ℕ)) |
85 | 78, 82, 84 | sylanbrc 695 |
. . . 4
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) →
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ)) |
86 | 75, 85 | jca 553 |
. . 3
⊢ ((𝐺 ∈ Abel ∧ 𝑥 ∈ (◡𝑂 “ ℕ)) → (∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))) |
87 | 86 | ralrimiva 2949 |
. 2
⊢ (𝐺 ∈ Abel →
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))) |
88 | 2, 28, 76 | issubg2 17432 |
. . 3
⊢ (𝐺 ∈ Grp → ((◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺) ↔ ((◡𝑂 “ ℕ) ⊆ (Base‘𝐺) ∧ (◡𝑂 “ ℕ) ≠ ∅ ∧
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))))) |
89 | 8, 88 | syl 17 |
. 2
⊢ (𝐺 ∈ Abel → ((◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺) ↔ ((◡𝑂 “ ℕ) ⊆ (Base‘𝐺) ∧ (◡𝑂 “ ℕ) ≠ ∅ ∧
∀𝑥 ∈ (◡𝑂 “ ℕ)(∀𝑦 ∈ (◡𝑂 “ ℕ)(𝑥(+g‘𝐺)𝑦) ∈ (◡𝑂 “ ℕ) ∧
((invg‘𝐺)‘𝑥) ∈ (◡𝑂 “ ℕ))))) |
90 | 7, 22, 87, 89 | mpbir3and 1238 |
1
⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺)) |