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 \in Abel \to O^{-1} [ℕ] \in SubGrp (G)$

Proof

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

Metamath Proof Explorer

Theorem torsubg

Proof