pgpfaclem2

	Ref	Expression
Hypotheses	pgpfac.b	$⊢ B = {Base}_{G}$
	pgpfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
	pgpfac.g	$⊢ φ \to G \in Abel$
	pgpfac.p	$⊢ φ \to P pGrp G$
	pgpfac.f	$⊢ φ \to B \in Fin$
	pgpfac.u	$⊢ φ \to U \in SubGrp (G)$
	pgpfac.a	$⊢ φ \to \forall t \in SubGrp (G) (t \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = t))$
	pgpfac.h	$⊢ H = G ↾_{𝑠} U$
	pgpfac.k	$⊢ K = mrCls (SubGrp (H))$
	pgpfac.o	$⊢ O = od (H)$
	pgpfac.e	$⊢ E = gEx (H)$
	pgpfac.0	$⊢ \underset{˙}{0} = 0_{H}$
	pgpfac.l	$⊢ \underset{˙}{\oplus} = LSSum (H)$
	pgpfac.1	$⊢ φ \to E \neq 1$
	pgpfac.x	$⊢ φ \to X \in U$
	pgpfac.oe	$⊢ φ \to O (X) = E$
	pgpfac.w	$⊢ φ \to W \in SubGrp (H)$
	pgpfac.i	$⊢ φ \to K (\{X\}) \cap W = \{\underset{˙}{0}\}$
	pgpfac.s	$⊢ φ \to K (\{X\}) \underset{˙}{\oplus} W = U$
Assertion	pgpfaclem2	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$

Proof

Step	Hyp	Ref	Expression
1		pgpfac.b	$⊢ B = {Base}_{G}$
2		pgpfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		pgpfac.g	$⊢ φ \to G \in Abel$
4		pgpfac.p	$⊢ φ \to P pGrp G$
5		pgpfac.f	$⊢ φ \to B \in Fin$
6		pgpfac.u	$⊢ φ \to U \in SubGrp (G)$
7		pgpfac.a	$⊢ φ \to \forall t \in SubGrp (G) (t \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = t))$
8		pgpfac.h	$⊢ H = G ↾_{𝑠} U$
9		pgpfac.k	$⊢ K = mrCls (SubGrp (H))$
10		pgpfac.o	$⊢ O = od (H)$
11		pgpfac.e	$⊢ E = gEx (H)$
12		pgpfac.0	$⊢ \underset{˙}{0} = 0_{H}$
13		pgpfac.l	$⊢ \underset{˙}{\oplus} = LSSum (H)$
14		pgpfac.1	$⊢ φ \to E \neq 1$
15		pgpfac.x	$⊢ φ \to X \in U$
16		pgpfac.oe	$⊢ φ \to O (X) = E$
17		pgpfac.w	$⊢ φ \to W \in SubGrp (H)$
18		pgpfac.i	$⊢ φ \to K (\{X\}) \cap W = \{\underset{˙}{0}\}$
19		pgpfac.s	$⊢ φ \to K (\{X\}) \underset{˙}{\oplus} W = U$
20	8	subsubg	$⊢ U \in SubGrp (G) \to (W \in SubGrp (H) \leftrightarrow (W \in SubGrp (G) \land W \subseteq U))$
21	6 20	syl	$⊢ φ \to (W \in SubGrp (H) \leftrightarrow (W \in SubGrp (G) \land W \subseteq U))$
22	17 21	mpbid	$⊢ φ \to (W \in SubGrp (G) \land W \subseteq U)$
23	22	simprd	$⊢ φ \to W \subseteq U$
24	1	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
25	6 24	syl	$⊢ φ \to U \subseteq B$
26	5 25	ssfid	$⊢ φ \to U \in Fin$
27	26 23	ssfid	$⊢ φ \to W \in Fin$
28		hashcl	$⊢ W \in Fin \to \|W\| \in ℕ_{0}$
29	27 28	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
30	29	nn0red	$⊢ φ \to \|W\| \in ℝ$
31	12	fvexi	$⊢ \underset{˙}{0} \in V$
32		hashsng	$⊢ \underset{˙}{0} \in V \to \|\{\underset{˙}{0}\}\| = 1$
33	31 32	ax-mp	$⊢ \|\{\underset{˙}{0}\}\| = 1$
34		subgrcl	$⊢ W \in SubGrp (H) \to H \in Grp$
35		eqid	$⊢ {Base}_{H} = {Base}_{H}$
36	35	subgacs	$⊢ H \in Grp \to SubGrp (H) \in ACS ({Base}_{H})$
37		acsmre	$⊢ SubGrp (H) \in ACS ({Base}_{H}) \to SubGrp (H) \in Moore ({Base}_{H})$
38	17 34 36 37	4syl	$⊢ φ \to SubGrp (H) \in Moore ({Base}_{H})$
39	38 9	mrcssvd	$⊢ φ \to K (\{X\}) \subseteq {Base}_{H}$
40	8	subgbas	$⊢ U \in SubGrp (G) \to U = {Base}_{H}$
41	6 40	syl	$⊢ φ \to U = {Base}_{H}$
42	39 41	sseqtrrd	$⊢ φ \to K (\{X\}) \subseteq U$
43	26 42	ssfid	$⊢ φ \to K (\{X\}) \in Fin$
44	15 41	eleqtrd	$⊢ φ \to X \in {Base}_{H}$
45	9	mrcsncl	$⊢ (SubGrp (H) \in Moore ({Base}_{H}) \land X \in {Base}_{H}) \to K (\{X\}) \in SubGrp (H)$
46	38 44 45	syl2anc	$⊢ φ \to K (\{X\}) \in SubGrp (H)$
47	12	subg0cl	$⊢ K (\{X\}) \in SubGrp (H) \to \underset{˙}{0} \in K (\{X\})$
48	46 47	syl	$⊢ φ \to \underset{˙}{0} \in K (\{X\})$
49	48	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq K (\{X\})$
50	44	snssd	$⊢ φ \to \{X\} \subseteq {Base}_{H}$
51	38 9 50	mrcssidd	$⊢ φ \to \{X\} \subseteq K (\{X\})$
52		snssg	$⊢ X \in U \to (X \in K (\{X\}) \leftrightarrow \{X\} \subseteq K (\{X\}))$
53	15 52	syl	$⊢ φ \to (X \in K (\{X\}) \leftrightarrow \{X\} \subseteq K (\{X\}))$
54	51 53	mpbird	$⊢ φ \to X \in K (\{X\})$
55	16 14	eqnetrd	$⊢ φ \to O (X) \neq 1$
56	10 12	od1	$⊢ H \in Grp \to O (\underset{˙}{0}) = 1$
57	17 34 56	3syl	$⊢ φ \to O (\underset{˙}{0}) = 1$
58		elsni	$⊢ X \in \{\underset{˙}{0}\} \to X = \underset{˙}{0}$
59	58	fveqeq2d	$⊢ X \in \{\underset{˙}{0}\} \to (O (X) = 1 \leftrightarrow O (\underset{˙}{0}) = 1)$
60	57 59	syl5ibrcom	$⊢ φ \to (X \in \{\underset{˙}{0}\} \to O (X) = 1)$
61	60	necon3ad	$⊢ φ \to (O (X) \neq 1 \to \neg X \in \{\underset{˙}{0}\})$
62	55 61	mpd	$⊢ φ \to \neg X \in \{\underset{˙}{0}\}$
63	49 54 62	ssnelpssd	$⊢ φ \to \{\underset{˙}{0}\} \subset K (\{X\})$
64		php3	$⊢ (K (\{X\}) \in Fin \land \{\underset{˙}{0}\} \subset K (\{X\})) \to \{\underset{˙}{0}\} ≺ K (\{X\})$
65	43 63 64	syl2anc	$⊢ φ \to \{\underset{˙}{0}\} ≺ K (\{X\})$
66		snfi	$⊢ \{\underset{˙}{0}\} \in Fin$
67		hashsdom	$⊢ (\{\underset{˙}{0}\} \in Fin \land K (\{X\}) \in Fin) \to (\|\{\underset{˙}{0}\}\| < \|K (\{X\})\| \leftrightarrow \{\underset{˙}{0}\} ≺ K (\{X\}))$
68	66 43 67	sylancr	$⊢ φ \to (\|\{\underset{˙}{0}\}\| < \|K (\{X\})\| \leftrightarrow \{\underset{˙}{0}\} ≺ K (\{X\}))$
69	65 68	mpbird	$⊢ φ \to \|\{\underset{˙}{0}\}\| < \|K (\{X\})\|$
70	33 69	eqbrtrrid	$⊢ φ \to 1 < \|K (\{X\})\|$
71		1red	$⊢ φ \to 1 \in ℝ$
72		hashcl	$⊢ K (\{X\}) \in Fin \to \|K (\{X\})\| \in ℕ_{0}$
73	43 72	syl	$⊢ φ \to \|K (\{X\})\| \in ℕ_{0}$
74	73	nn0red	$⊢ φ \to \|K (\{X\})\| \in ℝ$
75	12	subg0cl	$⊢ W \in SubGrp (H) \to \underset{˙}{0} \in W$
76		ne0i	$⊢ \underset{˙}{0} \in W \to W \neq \emptyset$
77	17 75 76	3syl	$⊢ φ \to W \neq \emptyset$
78		hashnncl	$⊢ W \in Fin \to (\|W\| \in ℕ \leftrightarrow W \neq \emptyset)$
79	27 78	syl	$⊢ φ \to (\|W\| \in ℕ \leftrightarrow W \neq \emptyset)$
80	77 79	mpbird	$⊢ φ \to \|W\| \in ℕ$
81	80	nngt0d	$⊢ φ \to 0 < \|W\|$
82		ltmul1	$⊢ (1 \in ℝ \land \|K (\{X\})\| \in ℝ \land (\|W\| \in ℝ \land 0 < \|W\|)) \to (1 < \|K (\{X\})\| \leftrightarrow 1 \|W\| < \|K (\{X\})\| \|W\|)$
83	71 74 30 81 82	syl112anc	$⊢ φ \to (1 < \|K (\{X\})\| \leftrightarrow 1 \|W\| < \|K (\{X\})\| \|W\|)$
84	70 83	mpbid	$⊢ φ \to 1 \|W\| < \|K (\{X\})\| \|W\|$
85	30	recnd	$⊢ φ \to \|W\| \in ℂ$
86	85	mullidd	$⊢ φ \to 1 \|W\| = \|W\|$
87		eqid	$⊢ Cntz (H) = Cntz (H)$
88	8	subgabl	$⊢ (G \in Abel \land U \in SubGrp (G)) \to H \in Abel$
89	3 6 88	syl2anc	$⊢ φ \to H \in Abel$
90	87 89 46 17	ablcntzd	$⊢ φ \to K (\{X\}) \subseteq Cntz (H) (W)$
91	13 12 87 46 17 18 90 43 27	lsmhash	$⊢ φ \to \|K (\{X\}) \underset{˙}{\oplus} W\| = \|K (\{X\})\| \|W\|$
92	19	fveq2d	$⊢ φ \to \|K (\{X\}) \underset{˙}{\oplus} W\| = \|U\|$
93	91 92	eqtr3d	$⊢ φ \to \|K (\{X\})\| \|W\| = \|U\|$
94	84 86 93	3brtr3d	$⊢ φ \to \|W\| < \|U\|$
95	30 94	ltned	$⊢ φ \to \|W\| \neq \|U\|$
96		fveq2	$⊢ W = U \to \|W\| = \|U\|$
97	96	necon3i	$⊢ \|W\| \neq \|U\| \to W \neq U$
98	95 97	syl	$⊢ φ \to W \neq U$
99		df-pss	$⊢ W \subset U \leftrightarrow (W \subseteq U \land W \neq U)$
100	23 98 99	sylanbrc	$⊢ φ \to W \subset U$
101		psseq1	$⊢ t = W \to (t \subset U \leftrightarrow W \subset U)$
102		eqeq2	$⊢ t = W \to (G DProd s = t \leftrightarrow G DProd s = W)$
103	102	anbi2d	$⊢ t = W \to ((G dom DProd s \land G DProd s = t) \leftrightarrow (G dom DProd s \land G DProd s = W))$
104	103	rexbidv	$⊢ t = W \to (\exists s \in Word C (G dom DProd s \land G DProd s = t) \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = W))$
105	101 104	imbi12d	$⊢ t = W \to ((t \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \leftrightarrow (W \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = W)))$
106	22	simpld	$⊢ φ \to W \in SubGrp (G)$
107	105 7 106	rspcdva	$⊢ φ \to (W \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = W))$
108	100 107	mpd	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = W)$
109		breq2	$⊢ s = a \to (G dom DProd s \leftrightarrow G dom DProd a)$
110		oveq2	$⊢ s = a \to G DProd s = G DProd a$
111	110	eqeq1d	$⊢ s = a \to (G DProd s = W \leftrightarrow G DProd a = W)$
112	109 111	anbi12d	$⊢ s = a \to ((G dom DProd s \land G DProd s = W) \leftrightarrow (G dom DProd a \land G DProd a = W))$
113	112	cbvrexvw	$⊢ \exists s \in Word C (G dom DProd s \land G DProd s = W) \leftrightarrow \exists a \in Word C (G dom DProd a \land G DProd a = W)$
114	108 113	sylib	$⊢ φ \to \exists a \in Word C (G dom DProd a \land G DProd a = W)$
115	3	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to G \in Abel$
116	4	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to P pGrp G$
117	5	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to B \in Fin$
118	6	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to U \in SubGrp (G)$
119	7	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to \forall t \in SubGrp (G) (t \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = t))$
120	14	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to E \neq 1$
121	15	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to X \in U$
122	16	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to O (X) = E$
123	17	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to W \in SubGrp (H)$
124	18	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to K (\{X\}) \cap W = \{\underset{˙}{0}\}$
125	19	adantr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to K (\{X\}) \underset{˙}{\oplus} W = U$
126		simprl	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to a \in Word C$
127		simprrl	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to G dom DProd a$
128		simprrr	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to G DProd a = W$
129		eqid	$⊢ a ++ ⟨“ K (\{X\}) ”⟩ = a ++ ⟨“ K (\{X\}) ”⟩$
130	1 2 115 116 117 118 119 8 9 10 11 12 13 120 121 122 123 124 125 126 127 128 129	pgpfaclem1	$⊢ (φ \land (a \in Word C \land (G dom DProd a \land G DProd a = W))) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
131	114 130	rexlimddv	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$

Metamath Proof Explorer

Theorem pgpfaclem2

Proof