pgpfaclem1

	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$
	pgpfac.2	$⊢ φ \to S \in Word C$
	pgpfac.4	$⊢ φ \to G dom DProd S$
	pgpfac.5	$⊢ φ \to G DProd S = W$
	pgpfac.t	$⊢ T = S ++ ⟨“ K (\{X\}) ”⟩$
Assertion	pgpfaclem1	$⊢ φ \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		pgpfac.2	$⊢ φ \to S \in Word C$
21		pgpfac.4	$⊢ φ \to G dom DProd S$
22		pgpfac.5	$⊢ φ \to G DProd S = W$
23		pgpfac.t	$⊢ T = S ++ ⟨“ K (\{X\}) ”⟩$
24	8	subggrp	$⊢ U \in SubGrp (G) \to H \in Grp$
25	6 24	syl	$⊢ φ \to H \in Grp$
26		eqid	$⊢ {Base}_{H} = {Base}_{H}$
27	26	subgacs	$⊢ H \in Grp \to SubGrp (H) \in ACS ({Base}_{H})$
28	25 27	syl	$⊢ φ \to SubGrp (H) \in ACS ({Base}_{H})$
29	28	acsmred	$⊢ φ \to SubGrp (H) \in Moore ({Base}_{H})$
30	8	subgbas	$⊢ U \in SubGrp (G) \to U = {Base}_{H}$
31	6 30	syl	$⊢ φ \to U = {Base}_{H}$
32	15 31	eleqtrd	$⊢ φ \to X \in {Base}_{H}$
33	9	mrcsncl	$⊢ (SubGrp (H) \in Moore ({Base}_{H}) \land X \in {Base}_{H}) \to K (\{X\}) \in SubGrp (H)$
34	29 32 33	syl2anc	$⊢ φ \to K (\{X\}) \in SubGrp (H)$
35	8	subsubg	$⊢ U \in SubGrp (G) \to (K (\{X\}) \in SubGrp (H) \leftrightarrow (K (\{X\}) \in SubGrp (G) \land K (\{X\}) \subseteq U))$
36	6 35	syl	$⊢ φ \to (K (\{X\}) \in SubGrp (H) \leftrightarrow (K (\{X\}) \in SubGrp (G) \land K (\{X\}) \subseteq U))$
37	34 36	mpbid	$⊢ φ \to (K (\{X\}) \in SubGrp (G) \land K (\{X\}) \subseteq U)$
38	37	simpld	$⊢ φ \to K (\{X\}) \in SubGrp (G)$
39	8	oveq1i	$⊢ H ↾_{𝑠} K (\{X\}) = (G ↾_{𝑠} U) ↾_{𝑠} K (\{X\})$
40	37	simprd	$⊢ φ \to K (\{X\}) \subseteq U$
41		ressabs	$⊢ (U \in SubGrp (G) \land K (\{X\}) \subseteq U) \to (G ↾_{𝑠} U) ↾_{𝑠} K (\{X\}) = G ↾_{𝑠} K (\{X\})$
42	6 40 41	syl2anc	$⊢ φ \to (G ↾_{𝑠} U) ↾_{𝑠} K (\{X\}) = G ↾_{𝑠} K (\{X\})$
43	39 42	eqtrid	$⊢ φ \to H ↾_{𝑠} K (\{X\}) = G ↾_{𝑠} K (\{X\})$
44	26 9	cycsubgcyg2	$⊢ (H \in Grp \land X \in {Base}_{H}) \to H ↾_{𝑠} K (\{X\}) \in CycGrp$
45	25 32 44	syl2anc	$⊢ φ \to H ↾_{𝑠} K (\{X\}) \in CycGrp$
46	43 45	eqeltrrd	$⊢ φ \to G ↾_{𝑠} K (\{X\}) \in CycGrp$
47		pgpprm	$⊢ P pGrp G \to P \in ℙ$
48	4 47	syl	$⊢ φ \to P \in ℙ$
49		subgpgp	$⊢ (P pGrp G \land K (\{X\}) \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} K (\{X\}))$
50	4 38 49	syl2anc	$⊢ φ \to P pGrp (G ↾_{𝑠} K (\{X\}))$
51		brelrng	$⊢ (P \in ℙ \land G ↾_{𝑠} K (\{X\}) \in CycGrp \land P pGrp (G ↾_{𝑠} K (\{X\}))) \to G ↾_{𝑠} K (\{X\}) \in ran pGrp$
52	48 46 50 51	syl3anc	$⊢ φ \to G ↾_{𝑠} K (\{X\}) \in ran pGrp$
53	46 52	elind	$⊢ φ \to G ↾_{𝑠} K (\{X\}) \in (CycGrp \cap ran pGrp)$
54		oveq2	$⊢ r = K (\{X\}) \to G ↾_{𝑠} r = G ↾_{𝑠} K (\{X\})$
55	54	eleq1d	$⊢ r = K (\{X\}) \to (G ↾_{𝑠} r \in (CycGrp \cap ran pGrp) \leftrightarrow G ↾_{𝑠} K (\{X\}) \in (CycGrp \cap ran pGrp))$
56	55 2	elrab2	$⊢ K (\{X\}) \in C \leftrightarrow (K (\{X\}) \in SubGrp (G) \land G ↾_{𝑠} K (\{X\}) \in (CycGrp \cap ran pGrp))$
57	38 53 56	sylanbrc	$⊢ φ \to K (\{X\}) \in C$
58	23 20 57	cats1cld	$⊢ φ \to T \in Word C$
59		wrdf	$⊢ T \in Word C \to T : (0 ..^\|T\|) ⟶ C$
60	58 59	syl	$⊢ φ \to T : (0 ..^\|T\|) ⟶ C$
61	2	ssrab3	$⊢ C \subseteq SubGrp (G)$
62		fss	$⊢ (T : (0 ..^\|T\|) ⟶ C \land C \subseteq SubGrp (G)) \to T : (0 ..^\|T\|) ⟶ SubGrp (G)$
63	60 61 62	sylancl	$⊢ φ \to T : (0 ..^\|T\|) ⟶ SubGrp (G)$
64		lencl	$⊢ S \in Word C \to \|S\| \in ℕ_{0}$
65	20 64	syl	$⊢ φ \to \|S\| \in ℕ_{0}$
66	65	nn0zd	$⊢ φ \to \|S\| \in ℤ$
67		fzosn	$⊢ \|S\| \in ℤ \to (\|S\| ..^\|S\| + 1) = \{\|S\|\}$
68	66 67	syl	$⊢ φ \to (\|S\| ..^\|S\| + 1) = \{\|S\|\}$
69	68	ineq2d	$⊢ φ \to (0 ..^\|S\|) \cap (\|S\| ..^\|S\| + 1) = (0 ..^\|S\|) \cap \{\|S\|\}$
70		fzodisj	$⊢ (0 ..^\|S\|) \cap (\|S\| ..^\|S\| + 1) = \emptyset$
71	69 70	eqtr3di	$⊢ φ \to (0 ..^\|S\|) \cap \{\|S\|\} = \emptyset$
72	23	fveq2i	$⊢ \|T\| = \|S ++ ⟨“ K (\{X\}) ”⟩\|$
73	57	s1cld	$⊢ φ \to ⟨“ K (\{X\}) ”⟩ \in Word C$
74		ccatlen	$⊢ (S \in Word C \land ⟨“ K (\{X\}) ”⟩ \in Word C) \to \|S ++ ⟨“ K (\{X\}) ”⟩\| = \|S\| + \|⟨“ K (\{X\}) ”⟩\|$
75	20 73 74	syl2anc	$⊢ φ \to \|S ++ ⟨“ K (\{X\}) ”⟩\| = \|S\| + \|⟨“ K (\{X\}) ”⟩\|$
76	72 75	eqtrid	$⊢ φ \to \|T\| = \|S\| + \|⟨“ K (\{X\}) ”⟩\|$
77		s1len	$⊢ \|⟨“ K (\{X\}) ”⟩\| = 1$
78	77	oveq2i	$⊢ \|S\| + \|⟨“ K (\{X\}) ”⟩\| = \|S\| + 1$
79	76 78	eqtrdi	$⊢ φ \to \|T\| = \|S\| + 1$
80	79	oveq2d	$⊢ φ \to (0 ..^\|T\|) = (0 ..^\|S\| + 1)$
81		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
82	65 81	eleqtrdi	$⊢ φ \to \|S\| \in ℤ_{\geq 0}$
83		fzosplitsn	$⊢ \|S\| \in ℤ_{\geq 0} \to (0 ..^\|S\| + 1) = (0 ..^\|S\|) \cup \{\|S\|\}$
84	82 83	syl	$⊢ φ \to (0 ..^\|S\| + 1) = (0 ..^\|S\|) \cup \{\|S\|\}$
85	80 84	eqtrd	$⊢ φ \to (0 ..^\|T\|) = (0 ..^\|S\|) \cup \{\|S\|\}$
86		eqid	$⊢ Cntz (G) = Cntz (G)$
87		eqid	$⊢ 0_{G} = 0_{G}$
88		cats1un	$⊢ (S \in Word C \land K (\{X\}) \in C) \to S ++ ⟨“ K (\{X\}) ”⟩ = S \cup \{⟨\|S\|, K (\{X\})⟩\}$
89	20 57 88	syl2anc	$⊢ φ \to S ++ ⟨“ K (\{X\}) ”⟩ = S \cup \{⟨\|S\|, K (\{X\})⟩\}$
90	23 89	eqtrid	$⊢ φ \to T = S \cup \{⟨\|S\|, K (\{X\})⟩\}$
91	90	reseq1d	$⊢ φ \to {T ↾}_{(0 ..^\|S\|)} = {(S \cup \{⟨\|S\|, K (\{X\})⟩\}) ↾}_{(0 ..^\|S\|)}$
92		wrdfn	$⊢ S \in Word C \to S Fn (0 ..^\|S\|)$
93	20 92	syl	$⊢ φ \to S Fn (0 ..^\|S\|)$
94		fzonel	$⊢ \neg \|S\| \in (0 ..^\|S\|)$
95		fsnunres	$⊢ (S Fn (0 ..^\|S\|) \land \neg \|S\| \in (0 ..^\|S\|)) \to {(S \cup \{⟨\|S\|, K (\{X\})⟩\}) ↾}_{(0 ..^\|S\|)} = S$
96	93 94 95	sylancl	$⊢ φ \to {(S \cup \{⟨\|S\|, K (\{X\})⟩\}) ↾}_{(0 ..^\|S\|)} = S$
97	91 96	eqtrd	$⊢ φ \to {T ↾}_{(0 ..^\|S\|)} = S$
98	21 97	breqtrrd	$⊢ φ \to G dom DProd ({T ↾}_{(0 ..^\|S\|)})$
99		fvex	$⊢ \|S\| \in V$
100		dprdsn	$⊢ (\|S\| \in V \land K (\{X\}) \in SubGrp (G)) \to (G dom DProd \{⟨\|S\|, K (\{X\})⟩\} \land G DProd \{⟨\|S\|, K (\{X\})⟩\} = K (\{X\}))$
101	99 38 100	sylancr	$⊢ φ \to (G dom DProd \{⟨\|S\|, K (\{X\})⟩\} \land G DProd \{⟨\|S\|, K (\{X\})⟩\} = K (\{X\}))$
102	101	simpld	$⊢ φ \to G dom DProd \{⟨\|S\|, K (\{X\})⟩\}$
103		wrdfn	$⊢ T \in Word C \to T Fn (0 ..^\|T\|)$
104	58 103	syl	$⊢ φ \to T Fn (0 ..^\|T\|)$
105		ssun2	$⊢ \{\|S\|\} \subseteq (0 ..^\|S\|) \cup \{\|S\|\}$
106	99	snss	$⊢ \|S\| \in ((0 ..^\|S\|) \cup \{\|S\|\}) \leftrightarrow \{\|S\|\} \subseteq (0 ..^\|S\|) \cup \{\|S\|\}$
107	105 106	mpbir	$⊢ \|S\| \in ((0 ..^\|S\|) \cup \{\|S\|\})$
108	107 85	eleqtrrid	$⊢ φ \to \|S\| \in (0 ..^\|T\|)$
109		fnressn	$⊢ (T Fn (0 ..^\|T\|) \land \|S\| \in (0 ..^\|T\|)) \to {T ↾}_{\{\|S\|\}} = \{⟨\|S\|, T (\|S\|)⟩\}$
110	104 108 109	syl2anc	$⊢ φ \to {T ↾}_{\{\|S\|\}} = \{⟨\|S\|, T (\|S\|)⟩\}$
111	23	fveq1i	$⊢ T (\|S\|) = (S ++ ⟨“ K (\{X\}) ”⟩) (\|S\|)$
112	65	nn0cnd	$⊢ φ \to \|S\| \in ℂ$
113	112	addid2d	$⊢ φ \to 0 + \|S\| = \|S\|$
114	113	fveq2d	$⊢ φ \to (S ++ ⟨“ K (\{X\}) ”⟩) (0 + \|S\|) = (S ++ ⟨“ K (\{X\}) ”⟩) (\|S\|)$
115	111 114	eqtr4id	$⊢ φ \to T (\|S\|) = (S ++ ⟨“ K (\{X\}) ”⟩) (0 + \|S\|)$
116		1nn	$⊢ 1 \in ℕ$
117	77 116	eqeltri	$⊢ \|⟨“ K (\{X\}) ”⟩\| \in ℕ$
118		lbfzo0	$⊢ 0 \in (0 ..^\|⟨“ K (\{X\}) ”⟩\|) \leftrightarrow \|⟨“ K (\{X\}) ”⟩\| \in ℕ$
119	117 118	mpbir	$⊢ 0 \in (0 ..^\|⟨“ K (\{X\}) ”⟩\|)$
120	119	a1i	$⊢ φ \to 0 \in (0 ..^\|⟨“ K (\{X\}) ”⟩\|)$
121		ccatval3	$⊢ (S \in Word C \land ⟨“ K (\{X\}) ”⟩ \in Word C \land 0 \in (0 ..^\|⟨“ K (\{X\}) ”⟩\|)) \to (S ++ ⟨“ K (\{X\}) ”⟩) (0 + \|S\|) = ⟨“ K (\{X\}) ”⟩ (0)$
122	20 73 120 121	syl3anc	$⊢ φ \to (S ++ ⟨“ K (\{X\}) ”⟩) (0 + \|S\|) = ⟨“ K (\{X\}) ”⟩ (0)$
123		fvex	$⊢ K (\{X\}) \in V$
124		s1fv	$⊢ K (\{X\}) \in V \to ⟨“ K (\{X\}) ”⟩ (0) = K (\{X\})$
125	123 124	mp1i	$⊢ φ \to ⟨“ K (\{X\}) ”⟩ (0) = K (\{X\})$
126	115 122 125	3eqtrd	$⊢ φ \to T (\|S\|) = K (\{X\})$
127	126	opeq2d	$⊢ φ \to ⟨\|S\|, T (\|S\|)⟩ = ⟨\|S\|, K (\{X\})⟩$
128	127	sneqd	$⊢ φ \to \{⟨\|S\|, T (\|S\|)⟩\} = \{⟨\|S\|, K (\{X\})⟩\}$
129	110 128	eqtrd	$⊢ φ \to {T ↾}_{\{\|S\|\}} = \{⟨\|S\|, K (\{X\})⟩\}$
130	102 129	breqtrrd	$⊢ φ \to G dom DProd ({T ↾}_{\{\|S\|\}})$
131		dprdsubg	$⊢ G dom DProd ({T ↾}_{(0 ..^\|S\|)}) \to G DProd ({T ↾}_{(0 ..^\|S\|)}) \in SubGrp (G)$
132	98 131	syl	$⊢ φ \to G DProd ({T ↾}_{(0 ..^\|S\|)}) \in SubGrp (G)$
133		dprdsubg	$⊢ G dom DProd ({T ↾}_{\{\|S\|\}}) \to G DProd ({T ↾}_{\{\|S\|\}}) \in SubGrp (G)$
134	130 133	syl	$⊢ φ \to G DProd ({T ↾}_{\{\|S\|\}}) \in SubGrp (G)$
135	86 3 132 134	ablcntzd	$⊢ φ \to G DProd ({T ↾}_{(0 ..^\|S\|)}) \subseteq Cntz (G) (G DProd ({T ↾}_{\{\|S\|\}}))$
136	97	oveq2d	$⊢ φ \to G DProd ({T ↾}_{(0 ..^\|S\|)}) = G DProd S$
137	136 22	eqtrd	$⊢ φ \to G DProd ({T ↾}_{(0 ..^\|S\|)}) = W$
138	129	oveq2d	$⊢ φ \to G DProd ({T ↾}_{\{\|S\|\}}) = G DProd \{⟨\|S\|, K (\{X\})⟩\}$
139	101	simprd	$⊢ φ \to G DProd \{⟨\|S\|, K (\{X\})⟩\} = K (\{X\})$
140	138 139	eqtrd	$⊢ φ \to G DProd ({T ↾}_{\{\|S\|\}}) = K (\{X\})$
141	137 140	ineq12d	$⊢ φ \to (G DProd ({T ↾}_{(0 ..^\|S\|)})) \cap (G DProd ({T ↾}_{\{\|S\|\}})) = W \cap K (\{X\})$
142		incom	$⊢ W \cap K (\{X\}) = K (\{X\}) \cap W$
143	141 142	eqtrdi	$⊢ φ \to (G DProd ({T ↾}_{(0 ..^\|S\|)})) \cap (G DProd ({T ↾}_{\{\|S\|\}})) = K (\{X\}) \cap W$
144	8 87	subg0	$⊢ U \in SubGrp (G) \to 0_{G} = 0_{H}$
145	6 144	syl	$⊢ φ \to 0_{G} = 0_{H}$
146	145 12	eqtr4di	$⊢ φ \to 0_{G} = \underset{˙}{0}$
147	146	sneqd	$⊢ φ \to \{0_{G}\} = \{\underset{˙}{0}\}$
148	18 143 147	3eqtr4d	$⊢ φ \to (G DProd ({T ↾}_{(0 ..^\|S\|)})) \cap (G DProd ({T ↾}_{\{\|S\|\}})) = \{0_{G}\}$
149	63 71 85 86 87 98 130 135 148	dmdprdsplit2	$⊢ φ \to G dom DProd T$
150		eqid	$⊢ LSSum (G) = LSSum (G)$
151	63 71 85 150 149	dprdsplit	$⊢ φ \to G DProd T = (G DProd ({T ↾}_{(0 ..^\|S\|)})) LSSum (G) (G DProd ({T ↾}_{\{\|S\|\}}))$
152	137 140	oveq12d	$⊢ φ \to (G DProd ({T ↾}_{(0 ..^\|S\|)})) LSSum (G) (G DProd ({T ↾}_{\{\|S\|\}})) = W LSSum (G) K (\{X\})$
153	137 132	eqeltrrd	$⊢ φ \to W \in SubGrp (G)$
154	150	lsmcom	$⊢ (G \in Abel \land W \in SubGrp (G) \land K (\{X\}) \in SubGrp (G)) \to W LSSum (G) K (\{X\}) = K (\{X\}) LSSum (G) W$
155	3 153 38 154	syl3anc	$⊢ φ \to W LSSum (G) K (\{X\}) = K (\{X\}) LSSum (G) W$
156	151 152 155	3eqtrd	$⊢ φ \to G DProd T = K (\{X\}) LSSum (G) W$
157	26	subgss	$⊢ W \in SubGrp (H) \to W \subseteq {Base}_{H}$
158	17 157	syl	$⊢ φ \to W \subseteq {Base}_{H}$
159	158 31	sseqtrrd	$⊢ φ \to W \subseteq U$
160	8 150 13	subglsm	$⊢ (U \in SubGrp (G) \land K (\{X\}) \subseteq U \land W \subseteq U) \to K (\{X\}) LSSum (G) W = K (\{X\}) \underset{˙}{\oplus} W$
161	6 40 159 160	syl3anc	$⊢ φ \to K (\{X\}) LSSum (G) W = K (\{X\}) \underset{˙}{\oplus} W$
162	156 161 19	3eqtrd	$⊢ φ \to G DProd T = U$
163		breq2	$⊢ s = T \to (G dom DProd s \leftrightarrow G dom DProd T)$
164		oveq2	$⊢ s = T \to G DProd s = G DProd T$
165	164	eqeq1d	$⊢ s = T \to (G DProd s = U \leftrightarrow G DProd T = U)$
166	163 165	anbi12d	$⊢ s = T \to ((G dom DProd s \land G DProd s = U) \leftrightarrow (G dom DProd T \land G DProd T = U))$
167	166	rspcev	$⊢ (T \in Word C \land (G dom DProd T \land G DProd T = U)) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
168	58 149 162 167	syl12anc	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$

Metamath Proof Explorer

Theorem pgpfaclem1

Proof