Metamath Proof Explorer

Theorem torsubg

Description: The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypothesis torsubg.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion torsubg ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 torsubg.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
2 cnvimass ⊢ ( ◡ 𝑂 “ ℕ ) ⊆ dom 𝑂
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 3 1 odf ⊢ 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0
5 4 fdmi ⊢ dom 𝑂 = ( Base ‘ 𝐺 )
6 2 5 sseqtri ⊢ ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 )
7 6 a1i ⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) )
8 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10 3 9 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
11 8 10 syl ⊢ ( 𝐺 ∈ Abel → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
12 1 9 od1 ⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
13 8 12 syl ⊢ ( 𝐺 ∈ Abel → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
14 1nn ⊢ 1 ∈ ℕ
15 13 14 eqeltrdi ⊢ ( 𝐺 ∈ Abel → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ )
16 ffn ⊢ ( 𝑂 : ( Base ‘ 𝐺 ) ⟶ ℕ0 → 𝑂 Fn ( Base ‘ 𝐺 ) )
17 4 16 ax-mp ⊢ 𝑂 Fn ( Base ‘ 𝐺 )
18 elpreima ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ ) ) )
19 17 18 ax-mp ⊢ ( ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∈ ℕ ) )
20 11 15 19 sylanbrc ⊢ ( 𝐺 ∈ Abel → ( 0g ‘ 𝐺 ) ∈ ( ◡ 𝑂 “ ℕ ) )
21 20 ne0d ⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ≠ ∅ )
22 8 ad2antrr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝐺 ∈ Grp )
23 6 sseli ⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
24 23 ad2antlr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
25 6 sseli ⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
26 25 adantl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
27 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28 3 27 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
29 22 24 26 28 syl3anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
30 0nnn ⊢ ¬ 0 ∈ ℕ
31 3 1 odcl ⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
32 24 31 syl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
33 32 nn0zd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ )
34 3 1 odcl ⊢ ( 𝑦 ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ0 )
35 26 34 syl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ0 )
36 35 nn0zd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℤ )
37 33 36 gcdcld ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ0 )
38 37 nn0cnd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ∈ ℂ )
39 38 mul02d ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) = 0 )
40 39 breq1d ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
41 33 36 zmulcld ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℤ )
42 0dvds ⊢ ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℤ → ( 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
43 41 42 syl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 0 ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
44 40 43 bitrd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 ) )
45 elpreima ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ℕ ) ) )
46 17 45 ax-mp ⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑥 ) ∈ ℕ ) )
47 46 simprbi ⊢ ( 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
48 47 ad2antlr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
49 elpreima ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑦 ) ∈ ℕ ) ) )
50 17 49 ax-mp ⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ 𝑦 ) ∈ ℕ ) )
51 50 simprbi ⊢ ( 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ )
52 51 adantl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑦 ) ∈ ℕ )
53 48 52 nnmulcld ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ )
54 eleq1 ⊢ ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 → ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ∈ ℕ ↔ 0 ∈ ℕ ) )
55 53 54 syl5ibcom ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) = 0 → 0 ∈ ℕ ) )
56 44 55 sylbid ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) → 0 ∈ ℕ ) )
57 30 56 mtoi ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ¬ ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
58 simpll ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → 𝐺 ∈ Abel )
59 1 3 27 odadd1 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
60 58 24 26 59 syl3anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) )
61 oveq1 ⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) = ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) )
62 61 breq1d ⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ↔ ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
63 60 62 syl5ibcom ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 → ( 0 · ( ( 𝑂 ‘ 𝑥 ) gcd ( 𝑂 ‘ 𝑦 ) ) ) ∥ ( ( 𝑂 ‘ 𝑥 ) · ( 𝑂 ‘ 𝑦 ) ) ) )
64 57 63 mtod ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ¬ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 )
65 3 1 odcl ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 )
66 29 65 syl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 )
67 elnn0 ⊢ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ∨ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
68 66 67 sylib ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ∨ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
69 68 ord ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ¬ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = 0 ) )
70 64 69 mt3d ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ )
71 elpreima ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ) ) )
72 17 71 ax-mp ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ℕ ) )
73 29 70 72 sylanbrc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) ∧ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) )
74 73 ralrimiva ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) )
75 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
76 3 75 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
77 8 23 76 syl2an ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) )
78 1 75 3 odinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑂 ‘ 𝑥 ) )
79 8 23 78 syl2an ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) = ( 𝑂 ‘ 𝑥 ) )
80 47 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ )
81 79 80 eqeltrd ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ )
82 elpreima ⊢ ( 𝑂 Fn ( Base ‘ 𝐺 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ ) ) )
83 17 82 ax-mp ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℕ ) )
84 77 81 83 sylanbrc ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) )
85 74 84 jca ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ) → ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) )
86 85 ralrimiva ⊢ ( 𝐺 ∈ Abel → ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) )
87 3 27 75 issubg2 ⊢ ( 𝐺 ∈ Grp → ( ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ◡ 𝑂 “ ℕ ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) ) ) )
88 8 87 syl ⊢ ( 𝐺 ∈ Abel → ( ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) ↔ ( ( ◡ 𝑂 “ ℕ ) ⊆ ( Base ‘ 𝐺 ) ∧ ( ◡ 𝑂 “ ℕ ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( ◡ 𝑂 “ ℕ ) ( ∀ 𝑦 ∈ ( ◡ 𝑂 “ ℕ ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝑂 “ ℕ ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( ◡ 𝑂 “ ℕ ) ) ) ) )
89 7 21 86 88 mpbir3and ⊢ ( 𝐺 ∈ Abel → ( ◡ 𝑂 “ ℕ ) ∈ ( SubGrp ‘ 𝐺 ) )