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 
|- O = ( od ` G )
Assertion torsubg 
|- ( G e. Abel -> ( `' O " NN ) e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 torsubg.1 
 |-  O = ( od ` G )
2 cnvimass 
 |-  ( `' O " NN ) C_ dom O
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 3 1 odf 
 |-  O : ( Base ` G ) --> NN0
5 4 fdmi 
 |-  dom O = ( Base ` G )
6 2 5 sseqtri 
 |-  ( `' O " NN ) C_ ( Base ` G )
7 6 a1i 
 |-  ( G e. Abel -> ( `' O " NN ) C_ ( Base ` G ) )
8 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
9 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
10 3 9 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
11 8 10 syl 
 |-  ( G e. Abel -> ( 0g ` G ) e. ( Base ` G ) )
12 1 9 od1 
 |-  ( G e. Grp -> ( O ` ( 0g ` G ) ) = 1 )
13 8 12 syl 
 |-  ( G e. Abel -> ( O ` ( 0g ` G ) ) = 1 )
14 1nn 
 |-  1 e. NN
15 13 14 eqeltrdi 
 |-  ( G e. Abel -> ( O ` ( 0g ` G ) ) e. NN )
16 ffn 
 |-  ( O : ( Base ` G ) --> NN0 -> O Fn ( Base ` G ) )
17 4 16 ax-mp 
 |-  O Fn ( Base ` G )
18 elpreima 
 |-  ( O Fn ( Base ` G ) -> ( ( 0g ` G ) e. ( `' O " NN ) <-> ( ( 0g ` G ) e. ( Base ` G ) /\ ( O ` ( 0g ` G ) ) e. NN ) ) )
19 17 18 ax-mp 
 |-  ( ( 0g ` G ) e. ( `' O " NN ) <-> ( ( 0g ` G ) e. ( Base ` G ) /\ ( O ` ( 0g ` G ) ) e. NN ) )
20 11 15 19 sylanbrc 
 |-  ( G e. Abel -> ( 0g ` G ) e. ( `' O " NN ) )
21 20 ne0d 
 |-  ( G e. Abel -> ( `' O " NN ) =/= (/) )
22 8 ad2antrr 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> G e. Grp )
23 6 sseli 
 |-  ( x e. ( `' O " NN ) -> x e. ( Base ` G ) )
24 23 ad2antlr 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> x e. ( Base ` G ) )
25 6 sseli 
 |-  ( y e. ( `' O " NN ) -> y e. ( Base ` G ) )
26 25 adantl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> y e. ( Base ` G ) )
27 eqid 
 |-  ( +g ` G ) = ( +g ` G )
28 3 27 grpcl 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
29 22 24 26 28 syl3anc 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
30 0nnn 
 |-  -. 0 e. NN
31 3 1 odcl 
 |-  ( x e. ( Base ` G ) -> ( O ` x ) e. NN0 )
32 24 31 syl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` x ) e. NN0 )
33 32 nn0zd 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` x ) e. ZZ )
34 3 1 odcl 
 |-  ( y e. ( Base ` G ) -> ( O ` y ) e. NN0 )
35 26 34 syl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` y ) e. NN0 )
36 35 nn0zd 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` y ) e. ZZ )
37 33 36 gcdcld 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` x ) gcd ( O ` y ) ) e. NN0 )
38 37 nn0cnd 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` x ) gcd ( O ` y ) ) e. CC )
39 38 mul02d 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) = 0 )
40 39 breq1d 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) <-> 0 || ( ( O ` x ) x. ( O ` y ) ) ) )
41 33 36 zmulcld 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` x ) x. ( O ` y ) ) e. ZZ )
42 0dvds 
 |-  ( ( ( O ` x ) x. ( O ` y ) ) e. ZZ -> ( 0 || ( ( O ` x ) x. ( O ` y ) ) <-> ( ( O ` x ) x. ( O ` y ) ) = 0 ) )
43 41 42 syl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( 0 || ( ( O ` x ) x. ( O ` y ) ) <-> ( ( O ` x ) x. ( O ` y ) ) = 0 ) )
44 40 43 bitrd 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) <-> ( ( O ` x ) x. ( O ` y ) ) = 0 ) )
45 elpreima 
 |-  ( O Fn ( Base ` G ) -> ( x e. ( `' O " NN ) <-> ( x e. ( Base ` G ) /\ ( O ` x ) e. NN ) ) )
46 17 45 ax-mp 
 |-  ( x e. ( `' O " NN ) <-> ( x e. ( Base ` G ) /\ ( O ` x ) e. NN ) )
47 46 simprbi 
 |-  ( x e. ( `' O " NN ) -> ( O ` x ) e. NN )
48 47 ad2antlr 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` x ) e. NN )
49 elpreima 
 |-  ( O Fn ( Base ` G ) -> ( y e. ( `' O " NN ) <-> ( y e. ( Base ` G ) /\ ( O ` y ) e. NN ) ) )
50 17 49 ax-mp 
 |-  ( y e. ( `' O " NN ) <-> ( y e. ( Base ` G ) /\ ( O ` y ) e. NN ) )
51 50 simprbi 
 |-  ( y e. ( `' O " NN ) -> ( O ` y ) e. NN )
52 51 adantl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` y ) e. NN )
53 48 52 nnmulcld 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` x ) x. ( O ` y ) ) e. NN )
54 eleq1 
 |-  ( ( ( O ` x ) x. ( O ` y ) ) = 0 -> ( ( ( O ` x ) x. ( O ` y ) ) e. NN <-> 0 e. NN ) )
55 53 54 syl5ibcom 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( ( O ` x ) x. ( O ` y ) ) = 0 -> 0 e. NN ) )
56 44 55 sylbid 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) -> 0 e. NN ) )
57 30 56 mtoi 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> -. ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) )
58 simpll 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> G e. Abel )
59 1 3 27 odadd1 
 |-  ( ( G e. Abel /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( ( O ` ( x ( +g ` G ) y ) ) x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) )
60 58 24 26 59 syl3anc 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` ( x ( +g ` G ) y ) ) x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) )
61 oveq1 
 |-  ( ( O ` ( x ( +g ` G ) y ) ) = 0 -> ( ( O ` ( x ( +g ` G ) y ) ) x. ( ( O ` x ) gcd ( O ` y ) ) ) = ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) )
62 61 breq1d 
 |-  ( ( O ` ( x ( +g ` G ) y ) ) = 0 -> ( ( ( O ` ( x ( +g ` G ) y ) ) x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) <-> ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) ) )
63 60 62 syl5ibcom 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` ( x ( +g ` G ) y ) ) = 0 -> ( 0 x. ( ( O ` x ) gcd ( O ` y ) ) ) || ( ( O ` x ) x. ( O ` y ) ) ) )
64 57 63 mtod 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> -. ( O ` ( x ( +g ` G ) y ) ) = 0 )
65 3 1 odcl 
 |-  ( ( x ( +g ` G ) y ) e. ( Base ` G ) -> ( O ` ( x ( +g ` G ) y ) ) e. NN0 )
66 29 65 syl 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` ( x ( +g ` G ) y ) ) e. NN0 )
67 elnn0 
 |-  ( ( O ` ( x ( +g ` G ) y ) ) e. NN0 <-> ( ( O ` ( x ( +g ` G ) y ) ) e. NN \/ ( O ` ( x ( +g ` G ) y ) ) = 0 ) )
68 66 67 sylib 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( ( O ` ( x ( +g ` G ) y ) ) e. NN \/ ( O ` ( x ( +g ` G ) y ) ) = 0 ) )
69 68 ord 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( -. ( O ` ( x ( +g ` G ) y ) ) e. NN -> ( O ` ( x ( +g ` G ) y ) ) = 0 ) )
70 64 69 mt3d 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( O ` ( x ( +g ` G ) y ) ) e. NN )
71 elpreima 
 |-  ( O Fn ( Base ` G ) -> ( ( x ( +g ` G ) y ) e. ( `' O " NN ) <-> ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ ( O ` ( x ( +g ` G ) y ) ) e. NN ) ) )
72 17 71 ax-mp 
 |-  ( ( x ( +g ` G ) y ) e. ( `' O " NN ) <-> ( ( x ( +g ` G ) y ) e. ( Base ` G ) /\ ( O ` ( x ( +g ` G ) y ) ) e. NN ) )
73 29 70 72 sylanbrc 
 |-  ( ( ( G e. Abel /\ x e. ( `' O " NN ) ) /\ y e. ( `' O " NN ) ) -> ( x ( +g ` G ) y ) e. ( `' O " NN ) )
74 73 ralrimiva 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> A. y e. ( `' O " NN ) ( x ( +g ` G ) y ) e. ( `' O " NN ) )
75 eqid 
 |-  ( invg ` G ) = ( invg ` G )
76 3 75 grpinvcl 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( invg ` G ) ` x ) e. ( Base ` G ) )
77 8 23 76 syl2an 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( ( invg ` G ) ` x ) e. ( Base ` G ) )
78 1 75 3 odinv 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( O ` ( ( invg ` G ) ` x ) ) = ( O ` x ) )
79 8 23 78 syl2an 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( O ` ( ( invg ` G ) ` x ) ) = ( O ` x ) )
80 47 adantl 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( O ` x ) e. NN )
81 79 80 eqeltrd 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( O ` ( ( invg ` G ) ` x ) ) e. NN )
82 elpreima 
 |-  ( O Fn ( Base ` G ) -> ( ( ( invg ` G ) ` x ) e. ( `' O " NN ) <-> ( ( ( invg ` G ) ` x ) e. ( Base ` G ) /\ ( O ` ( ( invg ` G ) ` x ) ) e. NN ) ) )
83 17 82 ax-mp 
 |-  ( ( ( invg ` G ) ` x ) e. ( `' O " NN ) <-> ( ( ( invg ` G ) ` x ) e. ( Base ` G ) /\ ( O ` ( ( invg ` G ) ` x ) ) e. NN ) )
84 77 81 83 sylanbrc 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( ( invg ` G ) ` x ) e. ( `' O " NN ) )
85 74 84 jca 
 |-  ( ( G e. Abel /\ x e. ( `' O " NN ) ) -> ( A. y e. ( `' O " NN ) ( x ( +g ` G ) y ) e. ( `' O " NN ) /\ ( ( invg ` G ) ` x ) e. ( `' O " NN ) ) )
86 85 ralrimiva 
 |-  ( G e. Abel -> A. x e. ( `' O " NN ) ( A. y e. ( `' O " NN ) ( x ( +g ` G ) y ) e. ( `' O " NN ) /\ ( ( invg ` G ) ` x ) e. ( `' O " NN ) ) )
87 3 27 75 issubg2 
 |-  ( G e. Grp -> ( ( `' O " NN ) e. ( SubGrp ` G ) <-> ( ( `' O " NN ) C_ ( Base ` G ) /\ ( `' O " NN ) =/= (/) /\ A. x e. ( `' O " NN ) ( A. y e. ( `' O " NN ) ( x ( +g ` G ) y ) e. ( `' O " NN ) /\ ( ( invg ` G ) ` x ) e. ( `' O " NN ) ) ) ) )
88 8 87 syl 
 |-  ( G e. Abel -> ( ( `' O " NN ) e. ( SubGrp ` G ) <-> ( ( `' O " NN ) C_ ( Base ` G ) /\ ( `' O " NN ) =/= (/) /\ A. x e. ( `' O " NN ) ( A. y e. ( `' O " NN ) ( x ( +g ` G ) y ) e. ( `' O " NN ) /\ ( ( invg ` G ) ` x ) e. ( `' O " NN ) ) ) ) )
89 7 21 86 88 mpbir3and 
 |-  ( G e. Abel -> ( `' O " NN ) e. ( SubGrp ` G ) )