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=odG
Assertion torsubg GAbelO-1SubGrpG

Proof

Step Hyp Ref Expression
1 torsubg.1 O=odG
2 cnvimass O-1domO
3 eqid BaseG=BaseG
4 3 1 odf O:BaseG0
5 4 fdmi domO=BaseG
6 2 5 sseqtri O-1BaseG
7 6 a1i GAbelO-1BaseG
8 ablgrp GAbelGGrp
9 eqid 0G=0G
10 3 9 grpidcl GGrp0GBaseG
11 8 10 syl GAbel0GBaseG
12 1 9 od1 GGrpO0G=1
13 8 12 syl GAbelO0G=1
14 1nn 1
15 13 14 eqeltrdi GAbelO0G
16 ffn O:BaseG0OFnBaseG
17 4 16 ax-mp OFnBaseG
18 elpreima OFnBaseG0GO-10GBaseGO0G
19 17 18 ax-mp 0GO-10GBaseGO0G
20 11 15 19 sylanbrc GAbel0GO-1
21 20 ne0d GAbelO-1
22 8 ad2antrr GAbelxO-1yO-1GGrp
23 6 sseli xO-1xBaseG
24 23 ad2antlr GAbelxO-1yO-1xBaseG
25 6 sseli yO-1yBaseG
26 25 adantl GAbelxO-1yO-1yBaseG
27 eqid +G=+G
28 3 27 grpcl GGrpxBaseGyBaseGx+GyBaseG
29 22 24 26 28 syl3anc GAbelxO-1yO-1x+GyBaseG
30 0nnn ¬0
31 3 1 odcl xBaseGOx0
32 24 31 syl GAbelxO-1yO-1Ox0
33 32 nn0zd GAbelxO-1yO-1Ox
34 3 1 odcl yBaseGOy0
35 26 34 syl GAbelxO-1yO-1Oy0
36 35 nn0zd GAbelxO-1yO-1Oy
37 33 36 gcdcld GAbelxO-1yO-1OxgcdOy0
38 37 nn0cnd GAbelxO-1yO-1OxgcdOy
39 38 mul02d GAbelxO-1yO-10OxgcdOy=0
40 39 breq1d GAbelxO-1yO-10OxgcdOyOxOy0OxOy
41 33 36 zmulcld GAbelxO-1yO-1OxOy
42 0dvds OxOy0OxOyOxOy=0
43 41 42 syl GAbelxO-1yO-10OxOyOxOy=0
44 40 43 bitrd GAbelxO-1yO-10OxgcdOyOxOyOxOy=0
45 elpreima OFnBaseGxO-1xBaseGOx
46 17 45 ax-mp xO-1xBaseGOx
47 46 simprbi xO-1Ox
48 47 ad2antlr GAbelxO-1yO-1Ox
49 elpreima OFnBaseGyO-1yBaseGOy
50 17 49 ax-mp yO-1yBaseGOy
51 50 simprbi yO-1Oy
52 51 adantl GAbelxO-1yO-1Oy
53 48 52 nnmulcld GAbelxO-1yO-1OxOy
54 eleq1 OxOy=0OxOy0
55 53 54 syl5ibcom GAbelxO-1yO-1OxOy=00
56 44 55 sylbid GAbelxO-1yO-10OxgcdOyOxOy0
57 30 56 mtoi GAbelxO-1yO-1¬0OxgcdOyOxOy
58 simpll GAbelxO-1yO-1GAbel
59 1 3 27 odadd1 GAbelxBaseGyBaseGOx+GyOxgcdOyOxOy
60 58 24 26 59 syl3anc GAbelxO-1yO-1Ox+GyOxgcdOyOxOy
61 oveq1 Ox+Gy=0Ox+GyOxgcdOy=0OxgcdOy
62 61 breq1d Ox+Gy=0Ox+GyOxgcdOyOxOy0OxgcdOyOxOy
63 60 62 syl5ibcom GAbelxO-1yO-1Ox+Gy=00OxgcdOyOxOy
64 57 63 mtod GAbelxO-1yO-1¬Ox+Gy=0
65 3 1 odcl x+GyBaseGOx+Gy0
66 29 65 syl GAbelxO-1yO-1Ox+Gy0
67 elnn0 Ox+Gy0Ox+GyOx+Gy=0
68 66 67 sylib GAbelxO-1yO-1Ox+GyOx+Gy=0
69 68 ord GAbelxO-1yO-1¬Ox+GyOx+Gy=0
70 64 69 mt3d GAbelxO-1yO-1Ox+Gy
71 elpreima OFnBaseGx+GyO-1x+GyBaseGOx+Gy
72 17 71 ax-mp x+GyO-1x+GyBaseGOx+Gy
73 29 70 72 sylanbrc GAbelxO-1yO-1x+GyO-1
74 73 ralrimiva GAbelxO-1yO-1x+GyO-1
75 eqid invgG=invgG
76 3 75 grpinvcl GGrpxBaseGinvgGxBaseG
77 8 23 76 syl2an GAbelxO-1invgGxBaseG
78 1 75 3 odinv GGrpxBaseGOinvgGx=Ox
79 8 23 78 syl2an GAbelxO-1OinvgGx=Ox
80 47 adantl GAbelxO-1Ox
81 79 80 eqeltrd GAbelxO-1OinvgGx
82 elpreima OFnBaseGinvgGxO-1invgGxBaseGOinvgGx
83 17 82 ax-mp invgGxO-1invgGxBaseGOinvgGx
84 77 81 83 sylanbrc GAbelxO-1invgGxO-1
85 74 84 jca GAbelxO-1yO-1x+GyO-1invgGxO-1
86 85 ralrimiva GAbelxO-1yO-1x+GyO-1invgGxO-1
87 3 27 75 issubg2 GGrpO-1SubGrpGO-1BaseGO-1xO-1yO-1x+GyO-1invgGxO-1
88 8 87 syl GAbelO-1SubGrpGO-1BaseGO-1xO-1yO-1x+GyO-1invgGxO-1
89 7 21 86 88 mpbir3and GAbelO-1SubGrpG