ablfaclem3

	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)\})$
Assertion	ablfaclem3	$⊢ φ \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		fzfid	$⊢ φ \to (1 \dots \|B\|) \in Fin$
10		prmnn	$⊢ w \in ℙ \to w \in ℕ$
11	10	3ad2ant2	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \in ℕ$
12		prmz	$⊢ w \in ℙ \to w \in ℤ$
13		ablgrp	$⊢ G \in Abel \to G \in Grp$
14	1	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
15	3 13 14	3syl	$⊢ φ \to B \neq \emptyset$
16		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
17	4 16	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
18	15 17	mpbird	$⊢ φ \to \|B\| \in ℕ$
19		dvdsle	$⊢ (w \in ℤ \land \|B\| \in ℕ) \to (w ∥ \|B\| \to w \leq \|B\|)$
20	12 18 19	syl2anr	$⊢ (φ \land w \in ℙ) \to (w ∥ \|B\| \to w \leq \|B\|)$
21	20	3impia	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \leq \|B\|$
22	18	nnzd	$⊢ φ \to \|B\| \in ℤ$
23	22	3ad2ant1	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to \|B\| \in ℤ$
24		fznn	$⊢ \|B\| \in ℤ \to (w \in (1 \dots \|B\|) \leftrightarrow (w \in ℕ \land w \leq \|B\|))$
25	23 24	syl	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to (w \in (1 \dots \|B\|) \leftrightarrow (w \in ℕ \land w \leq \|B\|))$
26	11 21 25	mpbir2and	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \in (1 \dots \|B\|)$
27	26	rabssdv	$⊢ φ \to \{w \in ℙ \| w ∥ \|B\|\} \subseteq (1 \dots \|B\|)$
28	6 27	eqsstrid	$⊢ φ \to A \subseteq (1 \dots \|B\|)$
29	9 28	ssfid	$⊢ φ \to A \in Fin$
30		dfin5	$⊢ Word C \cap W (S (q)) = \{y \in Word C \| y \in W (S (q))\}$
31	6	ssrab3	$⊢ A \subseteq ℙ$
32	31	a1i	$⊢ φ \to A \subseteq ℙ$
33	1 5 7 3 4 32	ablfac1b	$⊢ φ \to G dom DProd S$
34	1	fvexi	$⊢ B \in V$
35	34	rabex	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in V$
36	35 7	dmmpti	$⊢ dom S = A$
37	36	a1i	$⊢ φ \to dom S = A$
38	33 37	dprdf2	$⊢ φ \to S : A ⟶ SubGrp (G)$
39	38	ffvelrnda	$⊢ (φ \land q \in A) \to S (q) \in SubGrp (G)$
40	1 2 3 4 5 6 7 8	ablfaclem1	$⊢ S (q) \in SubGrp (G) \to W (S (q)) = \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\}$
41	39 40	syl	$⊢ (φ \land q \in A) \to W (S (q)) = \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\}$
42		ssrab2	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\} \subseteq Word C$
43	41 42	eqsstrdi	$⊢ (φ \land q \in A) \to W (S (q)) \subseteq Word C$
44		sseqin2	$⊢ W (S (q)) \subseteq Word C \leftrightarrow Word C \cap W (S (q)) = W (S (q))$
45	43 44	sylib	$⊢ (φ \land q \in A) \to Word C \cap W (S (q)) = W (S (q))$
46	30 45	syl5eqr	$⊢ (φ \land q \in A) \to \{y \in Word C \| y \in W (S (q))\} = W (S (q))$
47	46 41	eqtrd	$⊢ (φ \land q \in A) \to \{y \in Word C \| y \in W (S (q))\} = \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\}$
48		eqid	$⊢ {Base}_{(G ↾_{𝑠} S (q))} = {Base}_{(G ↾_{𝑠} S (q))}$
49		eqid	$⊢ \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} = \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
50		eqid	$⊢ G ↾_{𝑠} S (q) = G ↾_{𝑠} S (q)$
51	50	subgabl	$⊢ (G \in Abel \land S (q) \in SubGrp (G)) \to G ↾_{𝑠} S (q) \in Abel$
52	3 39 51	syl2an2r	$⊢ (φ \land q \in A) \to G ↾_{𝑠} S (q) \in Abel$
53	32	sselda	$⊢ (φ \land q \in A) \to q \in ℙ$
54	50	subgbas	$⊢ S (q) \in SubGrp (G) \to S (q) = {Base}_{(G ↾_{𝑠} S (q))}$
55	39 54	syl	$⊢ (φ \land q \in A) \to S (q) = {Base}_{(G ↾_{𝑠} S (q))}$
56	55	fveq2d	$⊢ (φ \land q \in A) \to \|S (q)\| = \|{Base}_{(G ↾_{𝑠} S (q))}\|$
57	1 5 7 3 4 32	ablfac1a	$⊢ (φ \land q \in A) \to \|S (q)\| = q^{q pCnt \|B\|}$
58	56 57	eqtr3d	$⊢ (φ \land q \in A) \to \|{Base}_{(G ↾_{𝑠} S (q))}\| = q^{q pCnt \|B\|}$
59	58	oveq2d	$⊢ (φ \land q \in A) \to q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\| = q pCnt q^{q pCnt \|B\|}$
60	18	adantr	$⊢ (φ \land q \in A) \to \|B\| \in ℕ$
61	53 60	pccld	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℕ_{0}$
62	61	nn0zd	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℤ$
63		pcid	$⊢ (q \in ℙ \land q pCnt \|B\| \in ℤ) \to q pCnt q^{q pCnt \|B\|} = q pCnt \|B\|$
64	53 62 63	syl2anc	$⊢ (φ \land q \in A) \to q pCnt q^{q pCnt \|B\|} = q pCnt \|B\|$
65	59 64	eqtrd	$⊢ (φ \land q \in A) \to q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\| = q pCnt \|B\|$
66	65	oveq2d	$⊢ (φ \land q \in A) \to q^{q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\|} = q^{q pCnt \|B\|}$
67	58 66	eqtr4d	$⊢ (φ \land q \in A) \to \|{Base}_{(G ↾_{𝑠} S (q))}\| = q^{q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\|}$
68	50	subggrp	$⊢ S (q) \in SubGrp (G) \to G ↾_{𝑠} S (q) \in Grp$
69	39 68	syl	$⊢ (φ \land q \in A) \to G ↾_{𝑠} S (q) \in Grp$
70	4	adantr	$⊢ (φ \land q \in A) \to B \in Fin$
71	1	subgss	$⊢ S (q) \in SubGrp (G) \to S (q) \subseteq B$
72	39 71	syl	$⊢ (φ \land q \in A) \to S (q) \subseteq B$
73	70 72	ssfid	$⊢ (φ \land q \in A) \to S (q) \in Fin$
74	55 73	eqeltrrd	$⊢ (φ \land q \in A) \to {Base}_{(G ↾_{𝑠} S (q))} \in Fin$
75	48	pgpfi2	$⊢ (G ↾_{𝑠} S (q) \in Grp \land {Base}_{(G ↾_{𝑠} S (q))} \in Fin) \to (q pGrp (G ↾_{𝑠} S (q)) \leftrightarrow (q \in ℙ \land \|{Base}_{(G ↾_{𝑠} S (q))}\| = q^{q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\|}))$
76	69 74 75	syl2anc	$⊢ (φ \land q \in A) \to (q pGrp (G ↾_{𝑠} S (q)) \leftrightarrow (q \in ℙ \land \|{Base}_{(G ↾_{𝑠} S (q))}\| = q^{q pCnt \|{Base}_{(G ↾_{𝑠} S (q))}\|}))$
77	53 67 76	mpbir2and	$⊢ (φ \land q \in A) \to q pGrp (G ↾_{𝑠} S (q))$
78	48 49 52 77 74	pgpfac	$⊢ (φ \land q \in A) \to \exists s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} ((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))})$
79		ssrab2	$⊢ \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq SubGrp (G ↾_{𝑠} S (q))$
80		sswrd	$⊢ \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq SubGrp (G ↾_{𝑠} S (q)) \to Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq Word SubGrp (G ↾_{𝑠} S (q))$
81	79 80	ax-mp	$⊢ Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq Word SubGrp (G ↾_{𝑠} S (q))$
82	81	sseli	$⊢ s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \to s \in Word SubGrp (G ↾_{𝑠} S (q))$
83	39	adantr	$⊢ ((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \to S (q) \in SubGrp (G)$
84	83	adantr	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to S (q) \in SubGrp (G)$
85	50	subgdmdprd	$⊢ S (q) \in SubGrp (G) \to ((G ↾_{𝑠} S (q)) dom DProd s \leftrightarrow (G dom DProd s \land ran s \subseteq 𝒫 S (q)))$
86	83 85	syl	$⊢ ((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \to ((G ↾_{𝑠} S (q)) dom DProd s \leftrightarrow (G dom DProd s \land ran s \subseteq 𝒫 S (q)))$
87	86	simprbda	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to G dom DProd s$
88	86	simplbda	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to ran s \subseteq 𝒫 S (q)$
89	50 84 87 88	subgdprd	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to (G ↾_{𝑠} S (q)) DProd s = G DProd s$
90	55	ad2antrr	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to S (q) = {Base}_{(G ↾_{𝑠} S (q))}$
91	90	eqcomd	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to {Base}_{(G ↾_{𝑠} S (q))} = S (q)$
92	89 91	eqeq12d	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to ((G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))} \leftrightarrow G DProd s = S (q))$
93	92	biimpd	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to ((G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))} \to G DProd s = S (q))$
94	93 87	jctild	$⊢ (((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \land (G ↾_{𝑠} S (q)) dom DProd s) \to ((G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))} \to (G dom DProd s \land G DProd s = S (q)))$
95	94	expimpd	$⊢ ((φ \land q \in A) \land s \in Word SubGrp (G ↾_{𝑠} S (q))) \to (((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))}) \to (G dom DProd s \land G DProd s = S (q)))$
96	82 95	sylan2	$⊢ ((φ \land q \in A) \land s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}) \to (((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))}) \to (G dom DProd s \land G DProd s = S (q)))$
97		oveq2	$⊢ r = y \to (G ↾_{𝑠} S (q)) ↾_{𝑠} r = (G ↾_{𝑠} S (q)) ↾_{𝑠} y$
98	97	eleq1d	$⊢ r = y \to ((G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp) \leftrightarrow (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp))$
99	98	cbvrabv	$⊢ \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} = \{y \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)\}$
100	50	subsubg	$⊢ S (q) \in SubGrp (G) \to (y \in SubGrp (G ↾_{𝑠} S (q)) \leftrightarrow (y \in SubGrp (G) \land y \subseteq S (q)))$
101	39 100	syl	$⊢ (φ \land q \in A) \to (y \in SubGrp (G ↾_{𝑠} S (q)) \leftrightarrow (y \in SubGrp (G) \land y \subseteq S (q)))$
102	101	simprbda	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q))) \to y \in SubGrp (G)$
103	102	3adant3	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to y \in SubGrp (G)$
104	39	3ad2ant1	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to S (q) \in SubGrp (G)$
105	101	simplbda	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q))) \to y \subseteq S (q)$
106	105	3adant3	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to y \subseteq S (q)$
107		ressabs	$⊢ (S (q) \in SubGrp (G) \land y \subseteq S (q)) \to (G ↾_{𝑠} S (q)) ↾_{𝑠} y = G ↾_{𝑠} y$
108	104 106 107	syl2anc	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to (G ↾_{𝑠} S (q)) ↾_{𝑠} y = G ↾_{𝑠} y$
109		simp3	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)$
110	108 109	eqeltrrd	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to G ↾_{𝑠} y \in (CycGrp \cap ran pGrp)$
111		oveq2	$⊢ r = y \to G ↾_{𝑠} r = G ↾_{𝑠} y$
112	111	eleq1d	$⊢ r = y \to (G ↾_{𝑠} r \in (CycGrp \cap ran pGrp) \leftrightarrow G ↾_{𝑠} y \in (CycGrp \cap ran pGrp))$
113	112 2	elrab2	$⊢ y \in C \leftrightarrow (y \in SubGrp (G) \land G ↾_{𝑠} y \in (CycGrp \cap ran pGrp))$
114	103 110 113	sylanbrc	$⊢ ((φ \land q \in A) \land y \in SubGrp (G ↾_{𝑠} S (q)) \land (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)) \to y \in C$
115	114	rabssdv	$⊢ (φ \land q \in A) \to \{y \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} y \in (CycGrp \cap ran pGrp)\} \subseteq C$
116	99 115	eqsstrid	$⊢ (φ \land q \in A) \to \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq C$
117		sswrd	$⊢ \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq C \to Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq Word C$
118	116 117	syl	$⊢ (φ \land q \in A) \to Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \subseteq Word C$
119	118	sselda	$⊢ ((φ \land q \in A) \land s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}) \to s \in Word C$
120	96 119	jctild	$⊢ ((φ \land q \in A) \land s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}) \to (((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))}) \to (s \in Word C \land (G dom DProd s \land G DProd s = S (q))))$
121	120	expimpd	$⊢ (φ \land q \in A) \to ((s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} \land ((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))})) \to (s \in Word C \land (G dom DProd s \land G DProd s = S (q))))$
122	121	reximdv2	$⊢ (φ \land q \in A) \to (\exists s \in Word \{r \in SubGrp (G ↾_{𝑠} S (q)) \| (G ↾_{𝑠} S (q)) ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\} ((G ↾_{𝑠} S (q)) dom DProd s \land (G ↾_{𝑠} S (q)) DProd s = {Base}_{(G ↾_{𝑠} S (q))}) \to \exists s \in Word C (G dom DProd s \land G DProd s = S (q)))$
123	78 122	mpd	$⊢ (φ \land q \in A) \to \exists s \in Word C (G dom DProd s \land G DProd s = S (q))$
124		rabn0	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\} \neq \emptyset \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = S (q))$
125	123 124	sylibr	$⊢ (φ \land q \in A) \to \{s \in Word C \| (G dom DProd s \land G DProd s = S (q))\} \neq \emptyset$
126	47 125	eqnetrd	$⊢ (φ \land q \in A) \to \{y \in Word C \| y \in W (S (q))\} \neq \emptyset$
127		rabn0	$⊢ \{y \in Word C \| y \in W (S (q))\} \neq \emptyset \leftrightarrow \exists y \in Word C y \in W (S (q))$
128	126 127	sylib	$⊢ (φ \land q \in A) \to \exists y \in Word C y \in W (S (q))$
129	128	ralrimiva	$⊢ φ \to \forall q \in A \exists y \in Word C y \in W (S (q))$
130		eleq1	$⊢ y = f (q) \to (y \in W (S (q)) \leftrightarrow f (q) \in W (S (q)))$
131	130	ac6sfi	$⊢ (A \in Fin \land \forall q \in A \exists y \in Word C y \in W (S (q))) \to \exists f (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))$
132	29 129 131	syl2anc	$⊢ φ \to \exists f (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))$
133		sneq	$⊢ q = y \to \{q\} = \{y\}$
134		fveq2	$⊢ q = y \to f (q) = f (y)$
135	134	dmeqd	$⊢ q = y \to dom f (q) = dom f (y)$
136	133 135	xpeq12d	$⊢ q = y \to \{q\} \times dom f (q) = \{y\} \times dom f (y)$
137	136	cbviunv	$⊢ ⋃_{q \in A} (\{q\} \times dom f (q)) = ⋃_{y \in A} (\{y\} \times dom f (y))$
138		snfi	$⊢ \{y\} \in Fin$
139		simprl	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to f : A ⟶ Word C$
140	139	ffvelrnda	$⊢ ((φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \land y \in A) \to f (y) \in Word C$
141		wrdf	$⊢ f (y) \in Word C \to f (y) : (0 ..^\|f (y)\|) ⟶ C$
142		fdm	$⊢ f (y) : (0 ..^\|f (y)\|) ⟶ C \to dom f (y) = (0 ..^\|f (y)\|)$
143	140 141 142	3syl	$⊢ ((φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \land y \in A) \to dom f (y) = (0 ..^\|f (y)\|)$
144		fzofi	$⊢ (0 ..^\|f (y)\|) \in Fin$
145	143 144	eqeltrdi	$⊢ ((φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \land y \in A) \to dom f (y) \in Fin$
146		xpfi	$⊢ (\{y\} \in Fin \land dom f (y) \in Fin) \to \{y\} \times dom f (y) \in Fin$
147	138 145 146	sylancr	$⊢ ((φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \land y \in A) \to \{y\} \times dom f (y) \in Fin$
148	147	ralrimiva	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to \forall y \in A \{y\} \times dom f (y) \in Fin$
149		iunfi	$⊢ (A \in Fin \land \forall y \in A \{y\} \times dom f (y) \in Fin) \to ⋃_{y \in A} (\{y\} \times dom f (y)) \in Fin$
150	29 148 149	syl2an2r	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to ⋃_{y \in A} (\{y\} \times dom f (y)) \in Fin$
151	137 150	eqeltrid	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to ⋃_{q \in A} (\{q\} \times dom f (q)) \in Fin$
152		hashcl	$⊢ ⋃_{q \in A} (\{q\} \times dom f (q)) \in Fin \to \|⋃_{q \in A} (\{q\} \times dom f (q))\| \in ℕ_{0}$
153		hashfzo0	$⊢ \|⋃_{q \in A} (\{q\} \times dom f (q))\| \in ℕ_{0} \to \|(0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|)\| = \|⋃_{q \in A} (\{q\} \times dom f (q))\|$
154	151 152 153	3syl	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to \|(0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|)\| = \|⋃_{q \in A} (\{q\} \times dom f (q))\|$
155		fzofi	$⊢ (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \in Fin$
156		hashen	$⊢ ((0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \in Fin \land ⋃_{q \in A} (\{q\} \times dom f (q)) \in Fin) \to (\|(0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|)\| = \|⋃_{q \in A} (\{q\} \times dom f (q))\| \leftrightarrow (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \approx ⋃_{q \in A} (\{q\} \times dom f (q)))$
157	155 151 156	sylancr	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to (\|(0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|)\| = \|⋃_{q \in A} (\{q\} \times dom f (q))\| \leftrightarrow (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \approx ⋃_{q \in A} (\{q\} \times dom f (q)))$
158	154 157	mpbid	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \approx ⋃_{q \in A} (\{q\} \times dom f (q))$
159		bren	$⊢ (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \approx ⋃_{q \in A} (\{q\} \times dom f (q)) \leftrightarrow \exists h h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q))$
160	158 159	sylib	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to \exists h h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q))$
161	3	adantr	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to G \in Abel$
162	4	adantr	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to B \in Fin$
163		breq1	$⊢ w = a \to (w ∥ \|B\| \leftrightarrow a ∥ \|B\|)$
164	163	cbvrabv	$⊢ \{w \in ℙ \| w ∥ \|B\|\} = \{a \in ℙ \| a ∥ \|B\|\}$
165	6 164	eqtri	$⊢ A = \{a \in ℙ \| a ∥ \|B\|\}$
166		fveq2	$⊢ x = c \to O (x) = O (c)$
167	166	breq1d	$⊢ x = c \to (O (x) ∥ p^{p pCnt \|B\|} \leftrightarrow O (c) ∥ p^{p pCnt \|B\|})$
168	167	cbvrabv	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} = \{c \in B \| O (c) ∥ p^{p pCnt \|B\|}\}$
169		id	$⊢ p = b \to p = b$
170		oveq1	$⊢ p = b \to p pCnt \|B\| = b pCnt \|B\|$
171	169 170	oveq12d	$⊢ p = b \to p^{p pCnt \|B\|} = b^{b pCnt \|B\|}$
172	171	breq2d	$⊢ p = b \to (O (c) ∥ p^{p pCnt \|B\|} \leftrightarrow O (c) ∥ b^{b pCnt \|B\|})$
173	172	rabbidv	$⊢ p = b \to \{c \in B \| O (c) ∥ p^{p pCnt \|B\|}\} = \{c \in B \| O (c) ∥ b^{b pCnt \|B\|}\}$
174	168 173	syl5eq	$⊢ p = b \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} = \{c \in B \| O (c) ∥ b^{b pCnt \|B\|}\}$
175	174	cbvmptv	$⊢ (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\}) = (b \in A ⟼ \{c \in B \| O (c) ∥ b^{b pCnt \|B\|}\})$
176	7 175	eqtri	$⊢ S = (b \in A ⟼ \{c \in B \| O (c) ∥ b^{b pCnt \|B\|}\})$
177		breq2	$⊢ s = t \to (G dom DProd s \leftrightarrow G dom DProd t)$
178		oveq2	$⊢ s = t \to G DProd s = G DProd t$
179	178	eqeq1d	$⊢ s = t \to (G DProd s = g \leftrightarrow G DProd t = g)$
180	177 179	anbi12d	$⊢ s = t \to ((G dom DProd s \land G DProd s = g) \leftrightarrow (G dom DProd t \land G DProd t = g))$
181	180	cbvrabv	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\} = \{t \in Word C \| (G dom DProd t \land G DProd t = g)\}$
182	181	mpteq2i	$⊢ (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\}) = (g \in SubGrp (G) ⟼ \{t \in Word C \| (G dom DProd t \land G DProd t = g)\})$
183	8 182	eqtri	$⊢ W = (g \in SubGrp (G) ⟼ \{t \in Word C \| (G dom DProd t \land G DProd t = g)\})$
184		simprll	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to f : A ⟶ Word C$
185		simprlr	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to \forall q \in A f (q) \in W (S (q))$
186		2fveq3	$⊢ q = y \to W (S (q)) = W (S (y))$
187	134 186	eleq12d	$⊢ q = y \to (f (q) \in W (S (q)) \leftrightarrow f (y) \in W (S (y)))$
188	187	cbvralvw	$⊢ \forall q \in A f (q) \in W (S (q)) \leftrightarrow \forall y \in A f (y) \in W (S (y))$
189	185 188	sylib	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to \forall y \in A f (y) \in W (S (y))$
190		simprr	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q))$
191	1 2 161 162 5 165 176 183 184 189 137 190	ablfaclem2	$⊢ (φ \land ((f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q))) \land h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)))) \to W (B) \neq \emptyset$
192	191	expr	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to (h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)) \to W (B) \neq \emptyset)$
193	192	exlimdv	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to (\exists h h : (0 ..^\|⋃_{q \in A} (\{q\} \times dom f (q))\|) \underset{1-1 onto}{⟶} ⋃_{q \in A} (\{q\} \times dom f (q)) \to W (B) \neq \emptyset)$
194	160 193	mpd	$⊢ (φ \land (f : A ⟶ Word C \land \forall q \in A f (q) \in W (S (q)))) \to W (B) \neq \emptyset$
195	132 194	exlimddv	$⊢ φ \to W (B) \neq \emptyset$

Metamath Proof Explorer

Theorem ablfaclem3

Proof