ablfacrp2

Description: The factors K , L of ablfacrp have the expected orders (which allows for repeated application to decompose G into subgroups of prime-power order). Lemma 6.1C.2 of Shapiro, p. 199. (Contributed by Mario Carneiro, 21-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$
Assertion	ablfacrp2	$⊢ φ \to (\|K\| = M \land \|L\| = N)$

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	6	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
11	7	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
12	10 11	nn0mulcld	$⊢ φ \to M \cdot N \in ℕ_{0}$
13	9 12	eqeltrd	$⊢ φ \to \|B\| \in ℕ_{0}$
14	1	fvexi	$⊢ B \in V$
15		hashclb	$⊢ B \in V \to (B \in Fin \leftrightarrow \|B\| \in ℕ_{0})$
16	14 15	ax-mp	$⊢ B \in Fin \leftrightarrow \|B\| \in ℕ_{0}$
17	13 16	sylibr	$⊢ φ \to B \in Fin$
18	3	ssrab3	$⊢ K \subseteq B$
19		ssfi	$⊢ (B \in Fin \land K \subseteq B) \to K \in Fin$
20	17 18 19	sylancl	$⊢ φ \to K \in Fin$
21		hashcl	$⊢ K \in Fin \to \|K\| \in ℕ_{0}$
22	20 21	syl	$⊢ φ \to \|K\| \in ℕ_{0}$
23	6	nnzd	$⊢ φ \to M \in ℤ$
24	2 1	oddvdssubg	$⊢ (G \in Abel \land M \in ℤ) \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
25	5 23 24	syl2anc	$⊢ φ \to \{x \in B \| O (x) ∥ M\} \in SubGrp (G)$
26	3 25	eqeltrid	$⊢ φ \to K \in SubGrp (G)$
27	1	lagsubg	$⊢ (K \in SubGrp (G) \land B \in Fin) \to \|K\| ∥ \|B\|$
28	26 17 27	syl2anc	$⊢ φ \to \|K\| ∥ \|B\|$
29	6	nncnd	$⊢ φ \to M \in ℂ$
30	7	nncnd	$⊢ φ \to N \in ℂ$
31	29 30	mulcomd	$⊢ φ \to M \cdot N = N \cdot M$
32	9 31	eqtrd	$⊢ φ \to \|B\| = N \cdot M$
33	28 32	breqtrd	$⊢ φ \to \|K\| ∥ N \cdot M$
34	1 2 3 4 5 6 7 8 9	ablfacrplem	$⊢ φ \to \|K\| \gcd N = 1$
35	22	nn0zd	$⊢ φ \to \|K\| \in ℤ$
36	7	nnzd	$⊢ φ \to N \in ℤ$
37		coprmdvds	$⊢ (\|K\| \in ℤ \land N \in ℤ \land M \in ℤ) \to ((\|K\| ∥ N \cdot M \land \|K\| \gcd N = 1) \to \|K\| ∥ M)$
38	35 36 23 37	syl3anc	$⊢ φ \to ((\|K\| ∥ N \cdot M \land \|K\| \gcd N = 1) \to \|K\| ∥ M)$
39	33 34 38	mp2and	$⊢ φ \to \|K\| ∥ M$
40	2 1	oddvdssubg	$⊢ (G \in Abel \land N \in ℤ) \to \{x \in B \| O (x) ∥ N\} \in SubGrp (G)$
41	5 36 40	syl2anc	$⊢ φ \to \{x \in B \| O (x) ∥ N\} \in SubGrp (G)$
42	4 41	eqeltrid	$⊢ φ \to L \in SubGrp (G)$
43	1	lagsubg	$⊢ (L \in SubGrp (G) \land B \in Fin) \to \|L\| ∥ \|B\|$
44	42 17 43	syl2anc	$⊢ φ \to \|L\| ∥ \|B\|$
45	44 9	breqtrd	$⊢ φ \to \|L\| ∥ M \cdot N$
46	23 36	gcdcomd	$⊢ φ \to M \gcd N = N \gcd M$
47	46 8	eqtr3d	$⊢ φ \to N \gcd M = 1$
48	1 2 4 3 5 7 6 47 32	ablfacrplem	$⊢ φ \to \|L\| \gcd M = 1$
49	4	ssrab3	$⊢ L \subseteq B$
50		ssfi	$⊢ (B \in Fin \land L \subseteq B) \to L \in Fin$
51	17 49 50	sylancl	$⊢ φ \to L \in Fin$
52		hashcl	$⊢ L \in Fin \to \|L\| \in ℕ_{0}$
53	51 52	syl	$⊢ φ \to \|L\| \in ℕ_{0}$
54	53	nn0zd	$⊢ φ \to \|L\| \in ℤ$
55		coprmdvds	$⊢ (\|L\| \in ℤ \land M \in ℤ \land N \in ℤ) \to ((\|L\| ∥ M \cdot N \land \|L\| \gcd M = 1) \to \|L\| ∥ N)$
56	54 23 36 55	syl3anc	$⊢ φ \to ((\|L\| ∥ M \cdot N \land \|L\| \gcd M = 1) \to \|L\| ∥ N)$
57	45 48 56	mp2and	$⊢ φ \to \|L\| ∥ N$
58		dvdscmul	$⊢ (\|L\| \in ℤ \land N \in ℤ \land M \in ℤ) \to (\|L\| ∥ N \to M \|L\| ∥ M \cdot N)$
59	54 36 23 58	syl3anc	$⊢ φ \to (\|L\| ∥ N \to M \|L\| ∥ M \cdot N)$
60	57 59	mpd	$⊢ φ \to M \|L\| ∥ M \cdot N$
61		eqid	$⊢ 0_{G} = 0_{G}$
62		eqid	$⊢ LSSum (G) = LSSum (G)$
63	1 2 3 4 5 6 7 8 9 61 62	ablfacrp	$⊢ φ \to (K \cap L = \{0_{G}\} \land K LSSum (G) L = B)$
64	63	simprd	$⊢ φ \to K LSSum (G) L = B$
65	64	fveq2d	$⊢ φ \to \|K LSSum (G) L\| = \|B\|$
66		eqid	$⊢ Cntz (G) = Cntz (G)$
67	63	simpld	$⊢ φ \to K \cap L = \{0_{G}\}$
68	66 5 26 42	ablcntzd	$⊢ φ \to K \subseteq Cntz (G) (L)$
69	62 61 66 26 42 67 68 20 51	lsmhash	$⊢ φ \to \|K LSSum (G) L\| = \|K\| \|L\|$
70	65 69	eqtr3d	$⊢ φ \to \|B\| = \|K\| \|L\|$
71	70 9	eqtr3d	$⊢ φ \to \|K\| \|L\| = M \cdot N$
72	60 71	breqtrrd	$⊢ φ \to M \|L\| ∥ \|K\| \|L\|$
73	61	subg0cl	$⊢ L \in SubGrp (G) \to 0_{G} \in L$
74		ne0i	$⊢ 0_{G} \in L \to L \neq \emptyset$
75	42 73 74	3syl	$⊢ φ \to L \neq \emptyset$
76		hashnncl	$⊢ L \in Fin \to (\|L\| \in ℕ \leftrightarrow L \neq \emptyset)$
77	51 76	syl	$⊢ φ \to (\|L\| \in ℕ \leftrightarrow L \neq \emptyset)$
78	75 77	mpbird	$⊢ φ \to \|L\| \in ℕ$
79	78	nnne0d	$⊢ φ \to \|L\| \neq 0$
80		dvdsmulcr	$⊢ (M \in ℤ \land \|K\| \in ℤ \land (\|L\| \in ℤ \land \|L\| \neq 0)) \to (M \|L\| ∥ \|K\| \|L\| \leftrightarrow M ∥ \|K\|)$
81	23 35 54 79 80	syl112anc	$⊢ φ \to (M \|L\| ∥ \|K\| \|L\| \leftrightarrow M ∥ \|K\|)$
82	72 81	mpbid	$⊢ φ \to M ∥ \|K\|$
83		dvdseq	$⊢ ((\|K\| \in ℕ_{0} \land M \in ℕ_{0}) \land (\|K\| ∥ M \land M ∥ \|K\|)) \to \|K\| = M$
84	22 10 39 82 83	syl22anc	$⊢ φ \to \|K\| = M$
85		dvdsmulc	$⊢ (\|K\| \in ℤ \land M \in ℤ \land N \in ℤ) \to (\|K\| ∥ M \to \|K\| \cdot N ∥ M \cdot N)$
86	35 23 36 85	syl3anc	$⊢ φ \to (\|K\| ∥ M \to \|K\| \cdot N ∥ M \cdot N)$
87	39 86	mpd	$⊢ φ \to \|K\| \cdot N ∥ M \cdot N$
88	87 71	breqtrrd	$⊢ φ \to \|K\| \cdot N ∥ \|K\| \|L\|$
89	84 6	eqeltrd	$⊢ φ \to \|K\| \in ℕ$
90	89	nnne0d	$⊢ φ \to \|K\| \neq 0$
91		dvdscmulr	$⊢ (N \in ℤ \land \|L\| \in ℤ \land (\|K\| \in ℤ \land \|K\| \neq 0)) \to (\|K\| \cdot N ∥ \|K\| \|L\| \leftrightarrow N ∥ \|L\|)$
92	36 54 35 90 91	syl112anc	$⊢ φ \to (\|K\| \cdot N ∥ \|K\| \|L\| \leftrightarrow N ∥ \|L\|)$
93	88 92	mpbid	$⊢ φ \to N ∥ \|L\|$
94		dvdseq	$⊢ ((\|L\| \in ℕ_{0} \land N \in ℕ_{0}) \land (\|L\| ∥ N \land N ∥ \|L\|)) \to \|L\| = N$
95	53 11 57 93 94	syl22anc	$⊢ φ \to \|L\| = N$
96	84 95	jca	$⊢ φ \to (\|K\| = M \land \|L\| = N)$

Metamath Proof Explorer

Theorem ablfacrp2

Proof