This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- O = ( od ` G )
oddvdssubg.1 
|- B = ( Base ` G )
Assertion oddvdssubg 
|- ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 torsubg.1 
 |-  O = ( od ` G )
2 oddvdssubg.1 
 |-  B = ( Base ` G )
3 ssrab2 
 |-  { x e. B | ( O ` x ) || N } C_ B
4 3 a1i 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } C_ B )
5 fveq2 
 |-  ( x = ( 0g ` G ) -> ( O ` x ) = ( O ` ( 0g ` G ) ) )
6 5 breq1d 
 |-  ( x = ( 0g ` G ) -> ( ( O ` x ) || N <-> ( O ` ( 0g ` G ) ) || N ) )
7 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
8 7 adantr 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> G e. Grp )
9 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
10 2 9 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. B )
11 8 10 syl 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> ( 0g ` G ) e. B )
12 1 9 od1 
 |-  ( G e. Grp -> ( O ` ( 0g ` G ) ) = 1 )
13 8 12 syl 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> ( O ` ( 0g ` G ) ) = 1 )
14 1dvds 
 |-  ( N e. ZZ -> 1 || N )
15 14 adantl 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> 1 || N )
16 13 15 eqbrtrd 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> ( O ` ( 0g ` G ) ) || N )
17 6 11 16 elrabd 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> ( 0g ` G ) e. { x e. B | ( O ` x ) || N } )
18 17 ne0d 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } =/= (/) )
19 fveq2 
 |-  ( x = y -> ( O ` x ) = ( O ` y ) )
20 19 breq1d 
 |-  ( x = y -> ( ( O ` x ) || N <-> ( O ` y ) || N ) )
21 20 elrab 
 |-  ( y e. { x e. B | ( O ` x ) || N } <-> ( y e. B /\ ( O ` y ) || N ) )
22 fveq2 
 |-  ( x = z -> ( O ` x ) = ( O ` z ) )
23 22 breq1d 
 |-  ( x = z -> ( ( O ` x ) || N <-> ( O ` z ) || N ) )
24 23 elrab 
 |-  ( z e. { x e. B | ( O ` x ) || N } <-> ( z e. B /\ ( O ` z ) || N ) )
25 fveq2 
 |-  ( x = ( y ( +g ` G ) z ) -> ( O ` x ) = ( O ` ( y ( +g ` G ) z ) ) )
26 25 breq1d 
 |-  ( x = ( y ( +g ` G ) z ) -> ( ( O ` x ) || N <-> ( O ` ( y ( +g ` G ) z ) ) || N ) )
27 8 adantr 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> G e. Grp )
28 27 adantr 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> G e. Grp )
29 simprl 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> y e. B )
30 29 adantr 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> y e. B )
31 simprl 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> z e. B )
32 eqid 
 |-  ( +g ` G ) = ( +g ` G )
33 2 32 grpcl 
 |-  ( ( G e. Grp /\ y e. B /\ z e. B ) -> ( y ( +g ` G ) z ) e. B )
34 28 30 31 33 syl3anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( y ( +g ` G ) z ) e. B )
35 simplll 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> G e. Abel )
36 simpllr 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> N e. ZZ )
37 eqid 
 |-  ( .g ` G ) = ( .g ` G )
38 2 37 32 mulgdi 
 |-  ( ( G e. Abel /\ ( N e. ZZ /\ y e. B /\ z e. B ) ) -> ( N ( .g ` G ) ( y ( +g ` G ) z ) ) = ( ( N ( .g ` G ) y ) ( +g ` G ) ( N ( .g ` G ) z ) ) )
39 35 36 30 31 38 syl13anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( N ( .g ` G ) ( y ( +g ` G ) z ) ) = ( ( N ( .g ` G ) y ) ( +g ` G ) ( N ( .g ` G ) z ) ) )
40 simprr 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( O ` y ) || N )
41 40 adantr 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( O ` y ) || N )
42 2 1 37 9 oddvds 
 |-  ( ( G e. Grp /\ y e. B /\ N e. ZZ ) -> ( ( O ` y ) || N <-> ( N ( .g ` G ) y ) = ( 0g ` G ) ) )
43 28 30 36 42 syl3anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( ( O ` y ) || N <-> ( N ( .g ` G ) y ) = ( 0g ` G ) ) )
44 41 43 mpbid 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( N ( .g ` G ) y ) = ( 0g ` G ) )
45 simprr 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( O ` z ) || N )
46 2 1 37 9 oddvds 
 |-  ( ( G e. Grp /\ z e. B /\ N e. ZZ ) -> ( ( O ` z ) || N <-> ( N ( .g ` G ) z ) = ( 0g ` G ) ) )
47 28 31 36 46 syl3anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( ( O ` z ) || N <-> ( N ( .g ` G ) z ) = ( 0g ` G ) ) )
48 45 47 mpbid 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( N ( .g ` G ) z ) = ( 0g ` G ) )
49 44 48 oveq12d 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( ( N ( .g ` G ) y ) ( +g ` G ) ( N ( .g ` G ) z ) ) = ( ( 0g ` G ) ( +g ` G ) ( 0g ` G ) ) )
50 28 10 syl 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( 0g ` G ) e. B )
51 2 32 9 grplid 
 |-  ( ( G e. Grp /\ ( 0g ` G ) e. B ) -> ( ( 0g ` G ) ( +g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
52 28 50 51 syl2anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( ( 0g ` G ) ( +g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
53 39 49 52 3eqtrd 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( N ( .g ` G ) ( y ( +g ` G ) z ) ) = ( 0g ` G ) )
54 2 1 37 9 oddvds 
 |-  ( ( G e. Grp /\ ( y ( +g ` G ) z ) e. B /\ N e. ZZ ) -> ( ( O ` ( y ( +g ` G ) z ) ) || N <-> ( N ( .g ` G ) ( y ( +g ` G ) z ) ) = ( 0g ` G ) ) )
55 28 34 36 54 syl3anc 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( ( O ` ( y ( +g ` G ) z ) ) || N <-> ( N ( .g ` G ) ( y ( +g ` G ) z ) ) = ( 0g ` G ) ) )
56 53 55 mpbird 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( O ` ( y ( +g ` G ) z ) ) || N )
57 26 34 56 elrabd 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ ( z e. B /\ ( O ` z ) || N ) ) -> ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } )
58 24 57 sylan2b 
 |-  ( ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) /\ z e. { x e. B | ( O ` x ) || N } ) -> ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } )
59 58 ralrimiva 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } )
60 fveq2 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( O ` x ) = ( O ` ( ( invg ` G ) ` y ) ) )
61 60 breq1d 
 |-  ( x = ( ( invg ` G ) ` y ) -> ( ( O ` x ) || N <-> ( O ` ( ( invg ` G ) ` y ) ) || N ) )
62 eqid 
 |-  ( invg ` G ) = ( invg ` G )
63 2 62 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( invg ` G ) ` y ) e. B )
64 27 29 63 syl2anc 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( ( invg ` G ) ` y ) e. B )
65 1 62 2 odinv 
 |-  ( ( G e. Grp /\ y e. B ) -> ( O ` ( ( invg ` G ) ` y ) ) = ( O ` y ) )
66 27 29 65 syl2anc 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( O ` ( ( invg ` G ) ` y ) ) = ( O ` y ) )
67 66 40 eqbrtrd 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( O ` ( ( invg ` G ) ` y ) ) || N )
68 61 64 67 elrabd 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } )
69 59 68 jca 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ ( y e. B /\ ( O ` y ) || N ) ) -> ( A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } /\ ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } ) )
70 21 69 sylan2b 
 |-  ( ( ( G e. Abel /\ N e. ZZ ) /\ y e. { x e. B | ( O ` x ) || N } ) -> ( A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } /\ ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } ) )
71 70 ralrimiva 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> A. y e. { x e. B | ( O ` x ) || N } ( A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } /\ ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } ) )
72 2 32 62 issubg2 
 |-  ( G e. Grp -> ( { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) <-> ( { x e. B | ( O ` x ) || N } C_ B /\ { x e. B | ( O ` x ) || N } =/= (/) /\ A. y e. { x e. B | ( O ` x ) || N } ( A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } /\ ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } ) ) ) )
73 8 72 syl 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> ( { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) <-> ( { x e. B | ( O ` x ) || N } C_ B /\ { x e. B | ( O ` x ) || N } =/= (/) /\ A. y e. { x e. B | ( O ` x ) || N } ( A. z e. { x e. B | ( O ` x ) || N } ( y ( +g ` G ) z ) e. { x e. B | ( O ` x ) || N } /\ ( ( invg ` G ) ` y ) e. { x e. B | ( O ` x ) || N } ) ) ) )
74 4 18 71 73 mpbir3and 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )