pgpfaclem3

	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))$
Assertion	pgpfaclem3	$⊢ φ \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		wrd0	$⊢ \emptyset \in Word C$
9		ablgrp	$⊢ G \in Abel \to G \in Grp$
10		eqid	$⊢ 0_{G} = 0_{G}$
11	10	dprd0	$⊢ G \in Grp \to (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\})$
12	3 9 11	3syl	$⊢ φ \to (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\})$
13	12	adantr	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\})$
14	10	subg0cl	$⊢ U \in SubGrp (G) \to 0_{G} \in U$
15	6 14	syl	$⊢ φ \to 0_{G} \in U$
16	15	adantr	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to 0_{G} \in U$
17		eqid	$⊢ G ↾_{𝑠} U = G ↾_{𝑠} U$
18	17	subgbas	$⊢ U \in SubGrp (G) \to U = {Base}_{(G ↾_{𝑠} U)}$
19	6 18	syl	$⊢ φ \to U = {Base}_{(G ↾_{𝑠} U)}$
20	19	adantr	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to U = {Base}_{(G ↾_{𝑠} U)}$
21	17	subggrp	$⊢ U \in SubGrp (G) \to G ↾_{𝑠} U \in Grp$
22	6 21	syl	$⊢ φ \to G ↾_{𝑠} U \in Grp$
23		grpmnd	$⊢ G ↾_{𝑠} U \in Grp \to G ↾_{𝑠} U \in Mnd$
24		eqid	$⊢ {Base}_{(G ↾_{𝑠} U)} = {Base}_{(G ↾_{𝑠} U)}$
25		eqid	$⊢ gEx (G ↾_{𝑠} U) = gEx (G ↾_{𝑠} U)$
26	24 25	gex1	$⊢ G ↾_{𝑠} U \in Mnd \to (gEx (G ↾_{𝑠} U) = 1 \leftrightarrow {Base}_{(G ↾_{𝑠} U)} \approx 1_{𝑜})$
27	22 23 26	3syl	$⊢ φ \to (gEx (G ↾_{𝑠} U) = 1 \leftrightarrow {Base}_{(G ↾_{𝑠} U)} \approx 1_{𝑜})$
28	27	biimpa	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to {Base}_{(G ↾_{𝑠} U)} \approx 1_{𝑜}$
29	20 28	eqbrtrd	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to U \approx 1_{𝑜}$
30		en1eqsn	$⊢ (0_{G} \in U \land U \approx 1_{𝑜}) \to U = \{0_{G}\}$
31	16 29 30	syl2anc	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to U = \{0_{G}\}$
32	31	eqeq2d	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to (G DProd \emptyset = U \leftrightarrow G DProd \emptyset = \{0_{G}\})$
33	32	anbi2d	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to ((G dom DProd \emptyset \land G DProd \emptyset = U) \leftrightarrow (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\}))$
34	13 33	mpbird	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to (G dom DProd \emptyset \land G DProd \emptyset = U)$
35		breq2	$⊢ s = \emptyset \to (G dom DProd s \leftrightarrow G dom DProd \emptyset)$
36		oveq2	$⊢ s = \emptyset \to G DProd s = G DProd \emptyset$
37	36	eqeq1d	$⊢ s = \emptyset \to (G DProd s = U \leftrightarrow G DProd \emptyset = U)$
38	35 37	anbi12d	$⊢ s = \emptyset \to ((G dom DProd s \land G DProd s = U) \leftrightarrow (G dom DProd \emptyset \land G DProd \emptyset = U))$
39	38	rspcev	$⊢ (\emptyset \in Word C \land (G dom DProd \emptyset \land G DProd \emptyset = U)) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
40	8 34 39	sylancr	$⊢ (φ \land gEx (G ↾_{𝑠} U) = 1) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
41	17	subgabl	$⊢ (G \in Abel \land U \in SubGrp (G)) \to G ↾_{𝑠} U \in Abel$
42	3 6 41	syl2anc	$⊢ φ \to G ↾_{𝑠} U \in Abel$
43	1	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
44	6 43	syl	$⊢ φ \to U \subseteq B$
45	5 44	ssfid	$⊢ φ \to U \in Fin$
46	19 45	eqeltrrd	$⊢ φ \to {Base}_{(G ↾_{𝑠} U)} \in Fin$
47	24 25	gexcl2	$⊢ (G ↾_{𝑠} U \in Grp \land {Base}_{(G ↾_{𝑠} U)} \in Fin) \to gEx (G ↾_{𝑠} U) \in ℕ$
48	22 46 47	syl2anc	$⊢ φ \to gEx (G ↾_{𝑠} U) \in ℕ$
49		eqid	$⊢ od (G ↾_{𝑠} U) = od (G ↾_{𝑠} U)$
50	24 25 49	gexex	$⊢ (G ↾_{𝑠} U \in Abel \land gEx (G ↾_{𝑠} U) \in ℕ) \to \exists x \in {Base}_{(G ↾_{𝑠} U)} od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U)$
51	42 48 50	syl2anc	$⊢ φ \to \exists x \in {Base}_{(G ↾_{𝑠} U)} od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U)$
52	51	adantr	$⊢ (φ \land gEx (G ↾_{𝑠} U) \neq 1) \to \exists x \in {Base}_{(G ↾_{𝑠} U)} od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U)$
53		eqid	$⊢ mrCls (SubGrp (G ↾_{𝑠} U)) = mrCls (SubGrp (G ↾_{𝑠} U))$
54		eqid	$⊢ mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) = mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\})$
55		eqid	$⊢ 0_{(G ↾_{𝑠} U)} = 0_{(G ↾_{𝑠} U)}$
56		eqid	$⊢ LSSum (G ↾_{𝑠} U) = LSSum (G ↾_{𝑠} U)$
57		subgpgp	$⊢ (P pGrp G \land U \in SubGrp (G)) \to P pGrp (G ↾_{𝑠} U)$
58	4 6 57	syl2anc	$⊢ φ \to P pGrp (G ↾_{𝑠} U)$
59	58	ad2antrr	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to P pGrp (G ↾_{𝑠} U)$
60	42	ad2antrr	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to G ↾_{𝑠} U \in Abel$
61	46	ad2antrr	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to {Base}_{(G ↾_{𝑠} U)} \in Fin$
62		simprr	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U)$
63		simprl	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to x \in {Base}_{(G ↾_{𝑠} U)}$
64	53 54 24 49 25 55 56 59 60 61 62 63	pgpfac1	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to \exists w \in SubGrp (G ↾_{𝑠} U) (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)})$
65	3	ad3antrrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to G \in Abel$
66	4	ad3antrrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to P pGrp G$
67	5	ad3antrrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to B \in Fin$
68	6	ad3antrrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to U \in SubGrp (G)$
69	7	ad3antrrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to \forall t \in SubGrp (G) (t \subset U \to \exists s \in Word C (G dom DProd s \land G DProd s = t))$
70		simpllr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to gEx (G ↾_{𝑠} U) \neq 1$
71		simplrl	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to x \in {Base}_{(G ↾_{𝑠} U)}$
72	68 18	syl	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to U = {Base}_{(G ↾_{𝑠} U)}$
73	71 72	eleqtrrd	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to x \in U$
74		simplrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U)$
75		simprl	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to w \in SubGrp (G ↾_{𝑠} U)$
76		simprrl	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\}$
77		simprrr	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}$
78	77 72	eqtr4d	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = U$
79	1 2 65 66 67 68 69 17 53 49 25 55 56 70 73 74 75 76 78	pgpfaclem2	$⊢ (((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \land (w \in SubGrp (G ↾_{𝑠} U) \land (mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) \cap w = \{0_{(G ↾_{𝑠} U)}\} \land mrCls (SubGrp (G ↾_{𝑠} U)) (\{x\}) LSSum (G ↾_{𝑠} U) w = {Base}_{(G ↾_{𝑠} U)}))) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
80	64 79	rexlimddv	$⊢ ((φ \land gEx (G ↾_{𝑠} U) \neq 1) \land (x \in {Base}_{(G ↾_{𝑠} U)} \land od (G ↾_{𝑠} U) (x) = gEx (G ↾_{𝑠} U))) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
81	52 80	rexlimddv	$⊢ (φ \land gEx (G ↾_{𝑠} U) \neq 1) \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$
82	40 81	pm2.61dane	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = U)$

Metamath Proof Explorer

Theorem pgpfaclem3

Proof