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 ) )