ablfaclem2

	Ref	Expression
Hypotheses	ablfac.b	$⊢ B = {Base}_{G}$
	ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
	ablfac.1	$⊢ φ \to G \in Abel$
	ablfac.2	$⊢ φ \to B \in Fin$
	ablfac.o	$⊢ O = od (G)$
	ablfac.a	$⊢ A = \{w \in ℙ \| w ∥ \|B\|\}$
	ablfac.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
	ablfac.w	$⊢ W = (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\})$
	ablfaclem2.f	$⊢ φ \to F : A ⟶ Word C$
	ablfaclem2.q	$⊢ φ \to \forall y \in A F (y) \in W (S (y))$
	ablfaclem2.l	$⊢ L = ⋃_{y \in A} (\{y\} \times dom F (y))$
	ablfaclem2.g	$⊢ φ \to H : (0 ..^\|L\|) \underset{1-1 onto}{⟶} L$
Assertion	ablfaclem2	$⊢ φ \to W (B) \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ablfac.b	$⊢ B = {Base}_{G}$
2		ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		ablfac.1	$⊢ φ \to G \in Abel$
4		ablfac.2	$⊢ φ \to B \in Fin$
5		ablfac.o	$⊢ O = od (G)$
6		ablfac.a	$⊢ A = \{w \in ℙ \| w ∥ \|B\|\}$
7		ablfac.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
8		ablfac.w	$⊢ W = (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\})$
9		ablfaclem2.f	$⊢ φ \to F : A ⟶ Word C$
10		ablfaclem2.q	$⊢ φ \to \forall y \in A F (y) \in W (S (y))$
11		ablfaclem2.l	$⊢ L = ⋃_{y \in A} (\{y\} \times dom F (y))$
12		ablfaclem2.g	$⊢ φ \to H : (0 ..^\|L\|) \underset{1-1 onto}{⟶} L$
13		ablgrp	$⊢ G \in Abel \to G \in Grp$
14	1	subgid	$⊢ G \in Grp \to B \in SubGrp (G)$
15	1 2 3 4 5 6 7 8	ablfaclem1	$⊢ B \in SubGrp (G) \to W (B) = \{s \in Word C \| (G dom DProd s \land G DProd s = B)\}$
16	3 13 14 15	4syl	$⊢ φ \to W (B) = \{s \in Word C \| (G dom DProd s \land G DProd s = B)\}$
17	9	ffvelcdmda	$⊢ (φ \land y \in A) \to F (y) \in Word C$
18		wrdf	$⊢ F (y) \in Word C \to F (y) : (0 ..^\|F (y)\|) ⟶ C$
19	17 18	syl	$⊢ (φ \land y \in A) \to F (y) : (0 ..^\|F (y)\|) ⟶ C$
20	19	ffdmd	$⊢ (φ \land y \in A) \to F (y) : dom F (y) ⟶ C$
21	20	ffvelcdmda	$⊢ ((φ \land y \in A) \land z \in dom F (y)) \to F (y) (z) \in C$
22	21	anasss	$⊢ (φ \land (y \in A \land z \in dom F (y))) \to F (y) (z) \in C$
23	22	ralrimivva	$⊢ φ \to \forall y \in A \forall z \in dom F (y) F (y) (z) \in C$
24		eqid	$⊢ (y \in A, z \in dom F (y) ⟼ F (y) (z)) = (y \in A, z \in dom F (y) ⟼ F (y) (z))$
25	24	fmpox	$⊢ \forall y \in A \forall z \in dom F (y) F (y) (z) \in C \leftrightarrow (y \in A, z \in dom F (y) ⟼ F (y) (z)) : ⋃_{y \in A} (\{y\} \times dom F (y)) ⟶ C$
26	23 25	sylib	$⊢ φ \to (y \in A, z \in dom F (y) ⟼ F (y) (z)) : ⋃_{y \in A} (\{y\} \times dom F (y)) ⟶ C$
27	11	feq2i	$⊢ (y \in A, z \in dom F (y) ⟼ F (y) (z)) : L ⟶ C \leftrightarrow (y \in A, z \in dom F (y) ⟼ F (y) (z)) : ⋃_{y \in A} (\{y\} \times dom F (y)) ⟶ C$
28	26 27	sylibr	$⊢ φ \to (y \in A, z \in dom F (y) ⟼ F (y) (z)) : L ⟶ C$
29		f1of	$⊢ H : (0 ..^\|L\|) \underset{1-1 onto}{⟶} L \to H : (0 ..^\|L\|) ⟶ L$
30	12 29	syl	$⊢ φ \to H : (0 ..^\|L\|) ⟶ L$
31		fco	$⊢ ((y \in A, z \in dom F (y) ⟼ F (y) (z)) : L ⟶ C \land H : (0 ..^\|L\|) ⟶ L) \to ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) : (0 ..^\|L\|) ⟶ C$
32	28 30 31	syl2anc	$⊢ φ \to ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) : (0 ..^\|L\|) ⟶ C$
33		iswrdi	$⊢ ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) : (0 ..^\|L\|) ⟶ C \to (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \in Word C$
34	32 33	syl	$⊢ φ \to (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \in Word C$
35	10	r19.21bi	$⊢ (φ \land y \in A) \to F (y) \in W (S (y))$
36	6	ssrab3	$⊢ A \subseteq ℙ$
37	36	a1i	$⊢ φ \to A \subseteq ℙ$
38	1 5 7 3 4 37	ablfac1b	$⊢ φ \to G dom DProd S$
39	1	fvexi	$⊢ B \in V$
40	39	rabex	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in V$
41	40 7	dmmpti	$⊢ dom S = A$
42	41	a1i	$⊢ φ \to dom S = A$
43	38 42	dprdf2	$⊢ φ \to S : A ⟶ SubGrp (G)$
44	43	ffvelcdmda	$⊢ (φ \land y \in A) \to S (y) \in SubGrp (G)$
45	1 2 3 4 5 6 7 8	ablfaclem1	$⊢ S (y) \in SubGrp (G) \to W (S (y)) = \{s \in Word C \| (G dom DProd s \land G DProd s = S (y))\}$
46	44 45	syl	$⊢ (φ \land y \in A) \to W (S (y)) = \{s \in Word C \| (G dom DProd s \land G DProd s = S (y))\}$
47	35 46	eleqtrd	$⊢ (φ \land y \in A) \to F (y) \in \{s \in Word C \| (G dom DProd s \land G DProd s = S (y))\}$
48		breq2	$⊢ s = F (y) \to (G dom DProd s \leftrightarrow G dom DProd F (y))$
49		oveq2	$⊢ s = F (y) \to G DProd s = G DProd F (y)$
50	49	eqeq1d	$⊢ s = F (y) \to (G DProd s = S (y) \leftrightarrow G DProd F (y) = S (y))$
51	48 50	anbi12d	$⊢ s = F (y) \to ((G dom DProd s \land G DProd s = S (y)) \leftrightarrow (G dom DProd F (y) \land G DProd F (y) = S (y)))$
52	51	elrab	$⊢ F (y) \in \{s \in Word C \| (G dom DProd s \land G DProd s = S (y))\} \leftrightarrow (F (y) \in Word C \land (G dom DProd F (y) \land G DProd F (y) = S (y)))$
53	52	simprbi	$⊢ F (y) \in \{s \in Word C \| (G dom DProd s \land G DProd s = S (y))\} \to (G dom DProd F (y) \land G DProd F (y) = S (y))$
54	47 53	syl	$⊢ (φ \land y \in A) \to (G dom DProd F (y) \land G DProd F (y) = S (y))$
55	54	simpld	$⊢ (φ \land y \in A) \to G dom DProd F (y)$
56		dprdf	$⊢ G dom DProd F (y) \to F (y) : dom F (y) ⟶ SubGrp (G)$
57	55 56	syl	$⊢ (φ \land y \in A) \to F (y) : dom F (y) ⟶ SubGrp (G)$
58	57	ffvelcdmda	$⊢ ((φ \land y \in A) \land z \in dom F (y)) \to F (y) (z) \in SubGrp (G)$
59	58	anasss	$⊢ (φ \land (y \in A \land z \in dom F (y))) \to F (y) (z) \in SubGrp (G)$
60	57	feqmptd	$⊢ (φ \land y \in A) \to F (y) = (z \in dom F (y) ⟼ F (y) (z))$
61	55 60	breqtrd	$⊢ (φ \land y \in A) \to G dom DProd (z \in dom F (y) ⟼ F (y) (z))$
62	43	feqmptd	$⊢ φ \to S = (y \in A ⟼ S (y))$
63	60	oveq2d	$⊢ (φ \land y \in A) \to G DProd F (y) = G DProd (z \in dom F (y) ⟼ F (y) (z))$
64	54	simprd	$⊢ (φ \land y \in A) \to G DProd F (y) = S (y)$
65	63 64	eqtr3d	$⊢ (φ \land y \in A) \to G DProd (z \in dom F (y) ⟼ F (y) (z)) = S (y)$
66	65	mpteq2dva	$⊢ φ \to (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z))) = (y \in A ⟼ S (y))$
67	62 66	eqtr4d	$⊢ φ \to S = (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z)))$
68	38 67	breqtrd	$⊢ φ \to G dom DProd (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z)))$
69	59 61 68	dprd2d2	$⊢ φ \to (G dom DProd (y \in A, z \in dom F (y) ⟼ F (y) (z)) \land G DProd (y \in A, z \in dom F (y) ⟼ F (y) (z)) = G DProd (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z))))$
70	69	simpld	$⊢ φ \to G dom DProd (y \in A, z \in dom F (y) ⟼ F (y) (z))$
71	28	fdmd	$⊢ φ \to dom (y \in A, z \in dom F (y) ⟼ F (y) (z)) = L$
72	70 71 12	dprdf1o	$⊢ φ \to (G dom DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) \land G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = G DProd (y \in A, z \in dom F (y) ⟼ F (y) (z)))$
73	72	simpld	$⊢ φ \to G dom DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H)$
74	72	simprd	$⊢ φ \to G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = G DProd (y \in A, z \in dom F (y) ⟼ F (y) (z))$
75	69	simprd	$⊢ φ \to G DProd (y \in A, z \in dom F (y) ⟼ F (y) (z)) = G DProd (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z)))$
76	67	oveq2d	$⊢ φ \to G DProd S = G DProd (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z)))$
77		ssidd	$⊢ φ \to A \subseteq A$
78	1 5 7 3 4 37 6 77	ablfac1c	$⊢ φ \to G DProd S = B$
79	76 78	eqtr3d	$⊢ φ \to G DProd (y \in A ⟼ G DProd (z \in dom F (y) ⟼ F (y) (z))) = B$
80	74 75 79	3eqtrd	$⊢ φ \to G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = B$
81		breq2	$⊢ s = (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \to (G dom DProd s \leftrightarrow G dom DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H))$
82		oveq2	$⊢ s = (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \to G DProd s = G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H)$
83	82	eqeq1d	$⊢ s = (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \to (G DProd s = B \leftrightarrow G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = B)$
84	81 83	anbi12d	$⊢ s = (y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \to ((G dom DProd s \land G DProd s = B) \leftrightarrow (G dom DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) \land G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = B))$
85	84	rspcev	$⊢ ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H \in Word C \land (G dom DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) \land G DProd ((y \in A, z \in dom F (y) ⟼ F (y) (z)) \circ H) = B)) \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$
86	34 73 80 85	syl12anc	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$
87		rabn0	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = B)\} \neq \emptyset \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = B)$
88	86 87	sylibr	$⊢ φ \to \{s \in Word C \| (G dom DProd s \land G DProd s = B)\} \neq \emptyset$
89	16 88	eqnetrd	$⊢ φ \to W (B) \neq \emptyset$

Metamath Proof Explorer

Theorem ablfaclem2

Proof