ablfacrp

Description: A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups K , L that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of Shapiro, p. 199. (Contributed by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	ablfacrp.b	$⊢ B = {Base}_{G}$
	ablfacrp.o	$⊢ O = od (G)$
	ablfacrp.k	$⊢ K = \{x \in B \| O (x) ∥ M\}$
	ablfacrp.l	$⊢ L = \{x \in B \| O (x) ∥ N\}$
	ablfacrp.g	$⊢ φ \to G \in Abel$
	ablfacrp.m	$⊢ φ \to M \in ℕ$
	ablfacrp.n	$⊢ φ \to N \in ℕ$
	ablfacrp.1	$⊢ φ \to M \gcd N = 1$
	ablfacrp.2	$⊢ φ \to \|B\| = M \cdot N$
	ablfacrp.z	$⊢ \underset{˙}{0} = 0_{G}$
	ablfacrp.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	ablfacrp	$⊢ φ \to (K \cap L = \{\underset{˙}{0}\} \land K \underset{˙}{\oplus} L = B)$

Proof

Step	Hyp	Ref	Expression
1		ablfacrp.b	$⊢ B = {Base}_{G}$
2		ablfacrp.o	$⊢ O = od (G)$
3		ablfacrp.k	$⊢ K = \{x \in B \| O (x) ∥ M\}$
4		ablfacrp.l	$⊢ L = \{x \in B \| O (x) ∥ N\}$
5		ablfacrp.g	$⊢ φ \to G \in Abel$
6		ablfacrp.m	$⊢ φ \to M \in ℕ$
7		ablfacrp.n	$⊢ φ \to N \in ℕ$
8		ablfacrp.1	$⊢ φ \to M \gcd N = 1$
9		ablfacrp.2	$⊢ φ \to \|B\| = M \cdot N$
10		ablfacrp.z	$⊢ \underset{˙}{0} = 0_{G}$
11		ablfacrp.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
12	3 4	ineq12i	$⊢ K \cap L = \{x \in B \| O (x) ∥ M\} \cap \{x \in B \| O (x) ∥ N\}$
13		inrab	$⊢ \{x \in B \| O (x) ∥ M\} \cap \{x \in B \| O (x) ∥ N\} = \{x \in B \| (O (x) ∥ M \land O (x) ∥ N)\}$
14	12 13	eqtri	$⊢ K \cap L = \{x \in B \| (O (x) ∥ M \land O (x) ∥ N)\}$
15	1 2	odcl	$⊢ x \in B \to O (x) \in ℕ_{0}$
16	15	adantl	$⊢ (φ \land x \in B) \to O (x) \in ℕ_{0}$
17	16	nn0zd	$⊢ (φ \land x \in B) \to O (x) \in ℤ$
18	6	nnzd	$⊢ φ \to M \in ℤ$
19	18	adantr	$⊢ (φ \land x \in B) \to M \in ℤ$
20	7	nnzd	$⊢ φ \to N \in ℤ$
21	20	adantr	$⊢ (φ \land x \in B) \to N \in ℤ$
22		dvdsgcd	$⊢ (O (x) \in ℤ \land M \in ℤ \land N \in ℤ) \to ((O (x) ∥ M \land O (x) ∥ N) \to O (x) ∥ (M \gcd N))$
23	17 19 21 22	syl3anc	$⊢ (φ \land x \in B) \to ((O (x) ∥ M \land O (x) ∥ N) \to O (x) ∥ (M \gcd N))$
24	23	3impia	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to O (x) ∥ (M \gcd N)$
25	8	3ad2ant1	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to M \gcd N = 1$
26	24 25	breqtrd	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to O (x) ∥ 1$
27		simp2	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to x \in B$
28		dvds1	$⊢ O (x) \in ℕ_{0} \to (O (x) ∥ 1 \leftrightarrow O (x) = 1)$
29	27 15 28	3syl	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to (O (x) ∥ 1 \leftrightarrow O (x) = 1)$
30	26 29	mpbid	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to O (x) = 1$
31		ablgrp	$⊢ G \in Abel \to G \in Grp$
32	5 31	syl	$⊢ φ \to G \in Grp$
33	32	3ad2ant1	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to G \in Grp$
34	2 10 1	odeq1	$⊢ (G \in Grp \land x \in B) \to (O (x) = 1 \leftrightarrow x = \underset{˙}{0})$
35	33 27 34	syl2anc	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to (O (x) = 1 \leftrightarrow x = \underset{˙}{0})$
36	30 35	mpbid	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to x = \underset{˙}{0}$
37		velsn	$⊢ x \in \{\underset{˙}{0}\} \leftrightarrow x = \underset{˙}{0}$
38	36 37	sylibr	$⊢ (φ \land x \in B \land (O (x) ∥ M \land O (x) ∥ N)) \to x \in \{\underset{˙}{0}\}$
39	38	rabssdv	$⊢ φ \to \{x \in B \| (O (x) ∥ M \land O (x) ∥ N)\} \subseteq \{\underset{˙}{0}\}$
40	14 39	eqsstrid	$⊢ φ \to K \cap L \subseteq \{\underset{˙}{0}\}$
41	2 1	oddvdssubg	$⊢ (G \in Abel \land M \in ℤ) \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
42	5 18 41	syl2anc	$⊢ φ \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
43	3 42	eqeltrid	$⊢ φ \to K \in SubGrp (G)$
44	10	subg0cl	$⊢ K \in SubGrp (G) \to \underset{˙}{0} \in K$
45	43 44	syl	$⊢ φ \to \underset{˙}{0} \in K$
46	2 1	oddvdssubg	$⊢ (G \in Abel \land N \in ℤ) \to \{x \in B \| O (x) ∥ N\} \in SubGrp (G)$
47	5 20 46	syl2anc	$⊢ φ \to \{x \in B \| O (x) ∥ N\} \in SubGrp (G)$
48	4 47	eqeltrid	$⊢ φ \to L \in SubGrp (G)$
49	10	subg0cl	$⊢ L \in SubGrp (G) \to \underset{˙}{0} \in L$
50	48 49	syl	$⊢ φ \to \underset{˙}{0} \in L$
51	45 50	elind	$⊢ φ \to \underset{˙}{0} \in (K \cap L)$
52	51	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq K \cap L$
53	40 52	eqssd	$⊢ φ \to K \cap L = \{\underset{˙}{0}\}$
54	11	lsmsubg2	$⊢ (G \in Abel \land K \in SubGrp (G) \land L \in SubGrp (G)) \to K \underset{˙}{\oplus} L \in SubGrp (G)$
55	5 43 48 54	syl3anc	$⊢ φ \to K \underset{˙}{\oplus} L \in SubGrp (G)$
56	1	subgss	$⊢ K \underset{˙}{\oplus} L \in SubGrp (G) \to K \underset{˙}{\oplus} L \subseteq B$
57	55 56	syl	$⊢ φ \to K \underset{˙}{\oplus} L \subseteq B$
58		eqid	$⊢ \cdot_{G} = \cdot_{G}$
59	1 58	mulg1	$⊢ g \in B \to 1 \cdot_{G} g = g$
60	59	adantl	$⊢ (φ \land g \in B) \to 1 \cdot_{G} g = g$
61		bezout	$⊢ (M \in ℤ \land N \in ℤ) \to \exists a \in ℤ \exists b \in ℤ M \gcd N = M a + N b$
62	18 20 61	syl2anc	$⊢ φ \to \exists a \in ℤ \exists b \in ℤ M \gcd N = M a + N b$
63	62	adantr	$⊢ (φ \land g \in B) \to \exists a \in ℤ \exists b \in ℤ M \gcd N = M a + N b$
64	8	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \gcd N = 1$
65	64	eqeq1d	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (M \gcd N = M a + N b \leftrightarrow 1 = M a + N b)$
66	18	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \in ℤ$
67		simprl	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
68	66 67	zmulcld	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M a \in ℤ$
69	68	zcnd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M a \in ℂ$
70	20	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N \in ℤ$
71		simprr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
72	70 71	zmulcld	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N b \in ℤ$
73	72	zcnd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N b \in ℂ$
74	69 73	addcomd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M a + N b = N b + M a$
75	74	oveq1d	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (M a + N b) \cdot_{G} g = (N b + M a) \cdot_{G} g$
76	32	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to G \in Grp$
77		simplr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to g \in B$
78		eqid	$⊢ +_{G} = +_{G}$
79	1 58 78	mulgdir	$⊢ (G \in Grp \land (N b \in ℤ \land M a \in ℤ \land g \in B)) \to (N b + M a) \cdot_{G} g = (N b \cdot_{G} g) +_{G} (M a \cdot_{G} g)$
80	76 72 68 77 79	syl13anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (N b + M a) \cdot_{G} g = (N b \cdot_{G} g) +_{G} (M a \cdot_{G} g)$
81	75 80	eqtrd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (M a + N b) \cdot_{G} g = (N b \cdot_{G} g) +_{G} (M a \cdot_{G} g)$
82	43	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to K \in SubGrp (G)$
83	48	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to L \in SubGrp (G)$
84	1 58	mulgcl	$⊢ (G \in Grp \land N b \in ℤ \land g \in B) \to N b \cdot_{G} g \in B$
85	76 72 77 84	syl3anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N b \cdot_{G} g \in B$
86	1 2	odcl	$⊢ g \in B \to O (g) \in ℕ_{0}$
87	86	ad2antlr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) \in ℕ_{0}$
88	87	nn0zd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) \in ℤ$
89	66 70	zmulcld	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \cdot N \in ℤ$
90	6 7	nnmulcld	$⊢ φ \to M \cdot N \in ℕ$
91	90	nnnn0d	$⊢ φ \to M \cdot N \in ℕ_{0}$
92	9 91	eqeltrd	$⊢ φ \to \|B\| \in ℕ_{0}$
93	1	fvexi	$⊢ B \in V$
94		hashclb	$⊢ B \in V \to (B \in Fin \leftrightarrow \|B\| \in ℕ_{0})$
95	93 94	ax-mp	$⊢ B \in Fin \leftrightarrow \|B\| \in ℕ_{0}$
96	92 95	sylibr	$⊢ φ \to B \in Fin$
97	96	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to B \in Fin$
98	1 2	oddvds2	$⊢ (G \in Grp \land B \in Fin \land g \in B) \to O (g) ∥ \|B\|$
99	76 97 77 98	syl3anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ \|B\|$
100	9	ad2antrr	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to \|B\| = M \cdot N$
101	99 100	breqtrd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ M \cdot N$
102	88 89 71 101	dvdsmultr1d	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ M \cdot N b$
103	66	zcnd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \in ℂ$
104	70	zcnd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N \in ℂ$
105	71	zcnd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
106	103 104 105	mulassd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \cdot N b = M N b$
107	102 106	breqtrd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ M N b$
108	1 2 58	odmulgid	$⊢ ((G \in Grp \land g \in B \land N b \in ℤ) \land M \in ℤ) \to (O (N b \cdot_{G} g) ∥ M \leftrightarrow O (g) ∥ M N b)$
109	76 77 72 66 108	syl31anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (O (N b \cdot_{G} g) ∥ M \leftrightarrow O (g) ∥ M N b)$
110	107 109	mpbird	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (N b \cdot_{G} g) ∥ M$
111		fveq2	$⊢ x = N b \cdot_{G} g \to O (x) = O (N b \cdot_{G} g)$
112	111	breq1d	$⊢ x = N b \cdot_{G} g \to (O (x) ∥ M \leftrightarrow O (N b \cdot_{G} g) ∥ M)$
113	112 3	elrab2	$⊢ N b \cdot_{G} g \in K \leftrightarrow (N b \cdot_{G} g \in B \land O (N b \cdot_{G} g) ∥ M)$
114	85 110 113	sylanbrc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to N b \cdot_{G} g \in K$
115	1 58	mulgcl	$⊢ (G \in Grp \land M a \in ℤ \land g \in B) \to M a \cdot_{G} g \in B$
116	76 68 77 115	syl3anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M a \cdot_{G} g \in B$
117	88 89 67 101	dvdsmultr1d	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ M \cdot N a$
118		zcn	$⊢ a \in ℤ \to a \in ℂ$
119	118	ad2antrl	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
120		mulass	$⊢ (M \in ℂ \land N \in ℂ \land a \in ℂ) \to M \cdot N a = M N a$
121		mul12	$⊢ (M \in ℂ \land N \in ℂ \land a \in ℂ) \to M N a = N M a$
122	120 121	eqtrd	$⊢ (M \in ℂ \land N \in ℂ \land a \in ℂ) \to M \cdot N a = N M a$
123	103 104 119 122	syl3anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M \cdot N a = N M a$
124	117 123	breqtrd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (g) ∥ N M a$
125	1 2 58	odmulgid	$⊢ ((G \in Grp \land g \in B \land M a \in ℤ) \land N \in ℤ) \to (O (M a \cdot_{G} g) ∥ N \leftrightarrow O (g) ∥ N M a)$
126	76 77 68 70 125	syl31anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (O (M a \cdot_{G} g) ∥ N \leftrightarrow O (g) ∥ N M a)$
127	124 126	mpbird	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to O (M a \cdot_{G} g) ∥ N$
128		fveq2	$⊢ x = M a \cdot_{G} g \to O (x) = O (M a \cdot_{G} g)$
129	128	breq1d	$⊢ x = M a \cdot_{G} g \to (O (x) ∥ N \leftrightarrow O (M a \cdot_{G} g) ∥ N)$
130	129 4	elrab2	$⊢ M a \cdot_{G} g \in L \leftrightarrow (M a \cdot_{G} g \in B \land O (M a \cdot_{G} g) ∥ N)$
131	116 127 130	sylanbrc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to M a \cdot_{G} g \in L$
132	78 11	lsmelvali	$⊢ ((K \in SubGrp (G) \land L \in SubGrp (G)) \land (N b \cdot_{G} g \in K \land M a \cdot_{G} g \in L)) \to (N b \cdot_{G} g) +_{G} (M a \cdot_{G} g) \in (K \underset{˙}{\oplus} L)$
133	82 83 114 131 132	syl22anc	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (N b \cdot_{G} g) +_{G} (M a \cdot_{G} g) \in (K \underset{˙}{\oplus} L)$
134	81 133	eqeltrd	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (M a + N b) \cdot_{G} g \in (K \underset{˙}{\oplus} L)$
135		oveq1	$⊢ 1 = M a + N b \to 1 \cdot_{G} g = (M a + N b) \cdot_{G} g$
136	135	eleq1d	$⊢ 1 = M a + N b \to (1 \cdot_{G} g \in (K \underset{˙}{\oplus} L) \leftrightarrow (M a + N b) \cdot_{G} g \in (K \underset{˙}{\oplus} L))$
137	134 136	syl5ibrcom	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (1 = M a + N b \to 1 \cdot_{G} g \in (K \underset{˙}{\oplus} L))$
138	65 137	sylbid	$⊢ ((φ \land g \in B) \land (a \in ℤ \land b \in ℤ)) \to (M \gcd N = M a + N b \to 1 \cdot_{G} g \in (K \underset{˙}{\oplus} L))$
139	138	rexlimdvva	$⊢ (φ \land g \in B) \to (\exists a \in ℤ \exists b \in ℤ M \gcd N = M a + N b \to 1 \cdot_{G} g \in (K \underset{˙}{\oplus} L))$
140	63 139	mpd	$⊢ (φ \land g \in B) \to 1 \cdot_{G} g \in (K \underset{˙}{\oplus} L)$
141	60 140	eqeltrrd	$⊢ (φ \land g \in B) \to g \in (K \underset{˙}{\oplus} L)$
142	57 141	eqelssd	$⊢ φ \to K \underset{˙}{\oplus} L = B$
143	53 142	jca	$⊢ φ \to (K \cap L = \{\underset{˙}{0}\} \land K \underset{˙}{\oplus} L = B)$

Metamath Proof Explorer

Theorem ablfacrp

Proof