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 \in Abel \land N \in ℤ) \to \{x \in B \| O (x) ∥ N\} \in SubGrp (G)$

Proof

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

Metamath Proof Explorer

Theorem oddvdssubg

Proof