ablfac1c

Description: The factors of ablfac1b cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	ablfac1.b	$⊢ B = {Base}_{G}$
	ablfac1.o	$⊢ O = od (G)$
	ablfac1.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
	ablfac1.g	$⊢ φ \to G \in Abel$
	ablfac1.f	$⊢ φ \to B \in Fin$
	ablfac1.1	$⊢ φ \to A \subseteq ℙ$
	ablfac1c.d	$⊢ D = \{w \in ℙ \| w ∥ \|B\|\}$
	ablfac1.2	$⊢ φ \to D \subseteq A$
Assertion	ablfac1c	$⊢ φ \to G DProd S = B$

Proof

Step	Hyp	Ref	Expression
1		ablfac1.b	$⊢ B = {Base}_{G}$
2		ablfac1.o	$⊢ O = od (G)$
3		ablfac1.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
4		ablfac1.g	$⊢ φ \to G \in Abel$
5		ablfac1.f	$⊢ φ \to B \in Fin$
6		ablfac1.1	$⊢ φ \to A \subseteq ℙ$
7		ablfac1c.d	$⊢ D = \{w \in ℙ \| w ∥ \|B\|\}$
8		ablfac1.2	$⊢ φ \to D \subseteq A$
9	1	dprdssv	$⊢ G DProd S \subseteq B$
10	9	a1i	$⊢ φ \to G DProd S \subseteq B$
11		ssfi	$⊢ (B \in Fin \land G DProd S \subseteq B) \to G DProd S \in Fin$
12	5 9 11	sylancl	$⊢ φ \to G DProd S \in Fin$
13		hashcl	$⊢ G DProd S \in Fin \to \|G DProd S\| \in ℕ_{0}$
14	12 13	syl	$⊢ φ \to \|G DProd S\| \in ℕ_{0}$
15		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
16	5 15	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
17	1 2 3 4 5 6	ablfac1b	$⊢ φ \to G dom DProd S$
18		dprdsubg	$⊢ G dom DProd S \to G DProd S \in SubGrp (G)$
19	17 18	syl	$⊢ φ \to G DProd S \in SubGrp (G)$
20	1	lagsubg	$⊢ (G DProd S \in SubGrp (G) \land B \in Fin) \to \|G DProd S\| ∥ \|B\|$
21	19 5 20	syl2anc	$⊢ φ \to \|G DProd S\| ∥ \|B\|$
22		breq1	$⊢ w = q \to (w ∥ \|B\| \leftrightarrow q ∥ \|B\|)$
23	22 7	elrab2	$⊢ q \in D \leftrightarrow (q \in ℙ \land q ∥ \|B\|)$
24	8	sseld	$⊢ φ \to (q \in D \to q \in A)$
25	23 24	syl5bir	$⊢ φ \to ((q \in ℙ \land q ∥ \|B\|) \to q \in A)$
26	25	impl	$⊢ ((φ \land q \in ℙ) \land q ∥ \|B\|) \to q \in A$
27	1 2 3 4 5 6	ablfac1a	$⊢ (φ \land q \in A) \to \|S (q)\| = q^{q pCnt \|B\|}$
28	1	fvexi	$⊢ B \in V$
29	28	rabex	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in V$
30	29 3	dmmpti	$⊢ dom S = A$
31	30	a1i	$⊢ φ \to dom S = A$
32	17 31	dprdf2	$⊢ φ \to S : A ⟶ SubGrp (G)$
33	32	ffvelrnda	$⊢ (φ \land q \in A) \to S (q) \in SubGrp (G)$
34	17	adantr	$⊢ (φ \land q \in A) \to G dom DProd S$
35	30	a1i	$⊢ (φ \land q \in A) \to dom S = A$
36		simpr	$⊢ (φ \land q \in A) \to q \in A$
37	34 35 36	dprdub	$⊢ (φ \land q \in A) \to S (q) \subseteq G DProd S$
38	19	adantr	$⊢ (φ \land q \in A) \to G DProd S \in SubGrp (G)$
39		eqid	$⊢ G ↾_{𝑠} (G DProd S) = G ↾_{𝑠} (G DProd S)$
40	39	subsubg	$⊢ G DProd S \in SubGrp (G) \to (S (q) \in SubGrp (G ↾_{𝑠} (G DProd S)) \leftrightarrow (S (q) \in SubGrp (G) \land S (q) \subseteq G DProd S))$
41	38 40	syl	$⊢ (φ \land q \in A) \to (S (q) \in SubGrp (G ↾_{𝑠} (G DProd S)) \leftrightarrow (S (q) \in SubGrp (G) \land S (q) \subseteq G DProd S))$
42	33 37 41	mpbir2and	$⊢ (φ \land q \in A) \to S (q) \in SubGrp (G ↾_{𝑠} (G DProd S))$
43	39	subgbas	$⊢ G DProd S \in SubGrp (G) \to G DProd S = {Base}_{(G ↾_{𝑠} (G DProd S))}$
44	38 43	syl	$⊢ (φ \land q \in A) \to G DProd S = {Base}_{(G ↾_{𝑠} (G DProd S))}$
45	12	adantr	$⊢ (φ \land q \in A) \to G DProd S \in Fin$
46	44 45	eqeltrrd	$⊢ (φ \land q \in A) \to {Base}_{(G ↾_{𝑠} (G DProd S))} \in Fin$
47		eqid	$⊢ {Base}_{(G ↾_{𝑠} (G DProd S))} = {Base}_{(G ↾_{𝑠} (G DProd S))}$
48	47	lagsubg	$⊢ (S (q) \in SubGrp (G ↾_{𝑠} (G DProd S)) \land {Base}_{(G ↾_{𝑠} (G DProd S))} \in Fin) \to \|S (q)\| ∥ \|{Base}_{(G ↾_{𝑠} (G DProd S))}\|$
49	42 46 48	syl2anc	$⊢ (φ \land q \in A) \to \|S (q)\| ∥ \|{Base}_{(G ↾_{𝑠} (G DProd S))}\|$
50	44	fveq2d	$⊢ (φ \land q \in A) \to \|G DProd S\| = \|{Base}_{(G ↾_{𝑠} (G DProd S))}\|$
51	49 50	breqtrrd	$⊢ (φ \land q \in A) \to \|S (q)\| ∥ \|G DProd S\|$
52	27 51	eqbrtrrd	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} ∥ \|G DProd S\|$
53	6	sselda	$⊢ (φ \land q \in A) \to q \in ℙ$
54	14	nn0zd	$⊢ φ \to \|G DProd S\| \in ℤ$
55	54	adantr	$⊢ (φ \land q \in A) \to \|G DProd S\| \in ℤ$
56		simpr	$⊢ (φ \land q \in ℙ) \to q \in ℙ$
57		ablgrp	$⊢ G \in Abel \to G \in Grp$
58	1	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
59	4 57 58	3syl	$⊢ φ \to B \neq \emptyset$
60		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
61	5 60	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
62	59 61	mpbird	$⊢ φ \to \|B\| \in ℕ$
63	62	adantr	$⊢ (φ \land q \in ℙ) \to \|B\| \in ℕ$
64	56 63	pccld	$⊢ (φ \land q \in ℙ) \to q pCnt \|B\| \in ℕ_{0}$
65	53 64	syldan	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℕ_{0}$
66		pcdvdsb	$⊢ (q \in ℙ \land \|G DProd S\| \in ℤ \land q pCnt \|B\| \in ℕ_{0}) \to (q pCnt \|B\| \leq q pCnt \|G DProd S\| \leftrightarrow q^{q pCnt \|B\|} ∥ \|G DProd S\|)$
67	53 55 65 66	syl3anc	$⊢ (φ \land q \in A) \to (q pCnt \|B\| \leq q pCnt \|G DProd S\| \leftrightarrow q^{q pCnt \|B\|} ∥ \|G DProd S\|)$
68	52 67	mpbird	$⊢ (φ \land q \in A) \to q pCnt \|B\| \leq q pCnt \|G DProd S\|$
69	68	adantlr	$⊢ ((φ \land q \in ℙ) \land q \in A) \to q pCnt \|B\| \leq q pCnt \|G DProd S\|$
70	26 69	syldan	$⊢ ((φ \land q \in ℙ) \land q ∥ \|B\|) \to q pCnt \|B\| \leq q pCnt \|G DProd S\|$
71		pceq0	$⊢ (q \in ℙ \land \|B\| \in ℕ) \to (q pCnt \|B\| = 0 \leftrightarrow \neg q ∥ \|B\|)$
72	56 63 71	syl2anc	$⊢ (φ \land q \in ℙ) \to (q pCnt \|B\| = 0 \leftrightarrow \neg q ∥ \|B\|)$
73	72	biimpar	$⊢ ((φ \land q \in ℙ) \land \neg q ∥ \|B\|) \to q pCnt \|B\| = 0$
74		eqid	$⊢ 0_{G} = 0_{G}$
75	74	subg0cl	$⊢ G DProd S \in SubGrp (G) \to 0_{G} \in (G DProd S)$
76		ne0i	$⊢ 0_{G} \in (G DProd S) \to G DProd S \neq \emptyset$
77	19 75 76	3syl	$⊢ φ \to G DProd S \neq \emptyset$
78		hashnncl	$⊢ G DProd S \in Fin \to (\|G DProd S\| \in ℕ \leftrightarrow G DProd S \neq \emptyset)$
79	12 78	syl	$⊢ φ \to (\|G DProd S\| \in ℕ \leftrightarrow G DProd S \neq \emptyset)$
80	77 79	mpbird	$⊢ φ \to \|G DProd S\| \in ℕ$
81	80	adantr	$⊢ (φ \land q \in ℙ) \to \|G DProd S\| \in ℕ$
82	56 81	pccld	$⊢ (φ \land q \in ℙ) \to q pCnt \|G DProd S\| \in ℕ_{0}$
83	82	nn0ge0d	$⊢ (φ \land q \in ℙ) \to 0 \leq q pCnt \|G DProd S\|$
84	83	adantr	$⊢ ((φ \land q \in ℙ) \land \neg q ∥ \|B\|) \to 0 \leq q pCnt \|G DProd S\|$
85	73 84	eqbrtrd	$⊢ ((φ \land q \in ℙ) \land \neg q ∥ \|B\|) \to q pCnt \|B\| \leq q pCnt \|G DProd S\|$
86	70 85	pm2.61dan	$⊢ (φ \land q \in ℙ) \to q pCnt \|B\| \leq q pCnt \|G DProd S\|$
87	86	ralrimiva	$⊢ φ \to \forall q \in ℙ q pCnt \|B\| \leq q pCnt \|G DProd S\|$
88	16	nn0zd	$⊢ φ \to \|B\| \in ℤ$
89		pc2dvds	$⊢ (\|B\| \in ℤ \land \|G DProd S\| \in ℤ) \to (\|B\| ∥ \|G DProd S\| \leftrightarrow \forall q \in ℙ q pCnt \|B\| \leq q pCnt \|G DProd S\|)$
90	88 54 89	syl2anc	$⊢ φ \to (\|B\| ∥ \|G DProd S\| \leftrightarrow \forall q \in ℙ q pCnt \|B\| \leq q pCnt \|G DProd S\|)$
91	87 90	mpbird	$⊢ φ \to \|B\| ∥ \|G DProd S\|$
92		dvdseq	$⊢ ((\|G DProd S\| \in ℕ_{0} \land \|B\| \in ℕ_{0}) \land (\|G DProd S\| ∥ \|B\| \land \|B\| ∥ \|G DProd S\|)) \to \|G DProd S\| = \|B\|$
93	14 16 21 91 92	syl22anc	$⊢ φ \to \|G DProd S\| = \|B\|$
94		hashen	$⊢ (G DProd S \in Fin \land B \in Fin) \to (\|G DProd S\| = \|B\| \leftrightarrow (G DProd S) \approx B)$
95	12 5 94	syl2anc	$⊢ φ \to (\|G DProd S\| = \|B\| \leftrightarrow (G DProd S) \approx B)$
96	93 95	mpbid	$⊢ φ \to (G DProd S) \approx B$
97		fisseneq	$⊢ (B \in Fin \land G DProd S \subseteq B \land (G DProd S) \approx B) \to G DProd S = B$
98	5 10 96 97	syl3anc	$⊢ φ \to G DProd S = B$

Metamath Proof Explorer

Theorem ablfac1c

Proof