Metamath Proof Explorer

Theorem oddvdssubg

Description: The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses torsubg.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
oddvdssubg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion oddvdssubg ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 torsubg.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
2 oddvdssubg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ⊆ 𝐵
4 3 a1i ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ⊆ 𝐵 )
5 fveq2 ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) )
6 5 breq1d ⊢ ( 𝑥 = ( 0g ‘ 𝐺 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∥ 𝑁 ) )
7 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
8 7 adantr ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → 𝐺 ∈ Grp )
9 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10 2 9 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
11 8 10 syl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
12 1 9 od1 ⊢ ( 𝐺 ∈ Grp → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
13 8 12 syl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) = 1 )
14 1dvds ⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
15 14 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → 1 ∥ 𝑁 )
16 13 15 eqbrtrd ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 0g ‘ 𝐺 ) ) ∥ 𝑁 )
17 6 11 16 elrabd ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ( 0g ‘ 𝐺 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
18 17 ne0d ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ≠ ∅ )
19 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑦 ) )
20 19 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) )
21 20 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) )
22 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑧 ) )
23 22 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) )
24 23 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ↔ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) )
25 fveq2 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
26 25 breq1d ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∥ 𝑁 ) )
27 8 adantr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → 𝐺 ∈ Grp )
28 27 adantr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → 𝐺 ∈ Grp )
29 simprl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → 𝑦 ∈ 𝐵 )
30 29 adantr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → 𝑦 ∈ 𝐵 )
31 simprl ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → 𝑧 ∈ 𝐵 )
32 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
33 2 32 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝐵 )
34 28 30 31 33 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝐵 )
35 simplll ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → 𝐺 ∈ Abel )
36 simpllr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → 𝑁 ∈ ℤ )
37 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
38 2 37 32 mulgdi ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) ) )
39 35 36 30 31 38 syl13anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) ) )
40 simprr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 )
41 40 adantr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 )
42 2 1 37 9 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
43 28 30 36 42 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) ) )
44 41 43 mpbid ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
45 simprr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 )
46 2 1 37 9 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) )
47 28 31 36 46 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) ) )
48 45 47 mpbid ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) = ( 0g ‘ 𝐺 ) )
49 44 48 oveq12d ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( ( 𝑁 ( .g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑁 ( .g ‘ 𝐺 ) 𝑧 ) ) = ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
50 28 10 syl ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
51 2 32 9 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
52 28 50 51 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( ( 0g ‘ 𝐺 ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
53 39 49 52 3eqtrd ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑁 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 0g ‘ 𝐺 ) )
54 2 1 37 9 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝐵 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 0g ‘ 𝐺 ) ) )
55 28 34 36 54 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( ( 𝑂 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( 0g ‘ 𝐺 ) ) )
56 53 55 mpbird ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ∥ 𝑁 )
57 26 34 56 elrabd ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑧 ) ∥ 𝑁 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
58 24 57 sylan2b ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) ∧ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
59 58 ralrimiva ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
60 fveq2 ⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
61 60 breq1d ⊢ ( 𝑥 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∥ 𝑁 ) )
62 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
63 2 62 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
64 27 29 63 syl2anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
65 1 62 2 odinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑂 ‘ 𝑦 ) )
66 27 29 65 syl2anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑂 ‘ 𝑦 ) )
67 66 40 eqbrtrd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∥ 𝑁 )
68 61 64 67 elrabd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
69 59 68 jca ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑂 ‘ 𝑦 ) ∥ 𝑁 ) ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) )
70 21 69 sylan2b ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) )
71 70 ralrimiva ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) )
72 2 32 62 issubg2 ⊢ ( 𝐺 ∈ Grp → ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ⊆ 𝐵 ∧ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ≠ ∅ ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ) ) )
73 8 72 syl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) ↔ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ⊆ 𝐵 ∧ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ≠ ∅ ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) ) ) )
74 4 18 71 73 mpbir3and ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )