Metamath Proof Explorer

Theorem pgpfaclem3

Description: Lemma for pgpfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses pgpfac.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
pgpfac.c ${⊢}{C}=\left\{{r}\in \mathrm{SubGrp}\left({G}\right)|{G}{↾}_{𝑠}{r}\in \left(\mathrm{CycGrp}\cap \mathrm{ran}\mathrm{pGrp}\right)\right\}$
pgpfac.g ${⊢}{\phi }\to {G}\in \mathrm{Abel}$
pgpfac.p ${⊢}{\phi }\to {P}\mathrm{pGrp}{G}$
pgpfac.f ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
pgpfac.u ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({G}\right)$
pgpfac.a ${⊢}{\phi }\to \forall {t}\in \mathrm{SubGrp}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left({t}\subset {U}\to \exists {s}\in \mathrm{Word}{C}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={t}\right)\right)$
Assertion pgpfaclem3 ${⊢}{\phi }\to \exists {s}\in \mathrm{Word}{C}\phantom{\rule{.4em}{0ex}}\left({G}\mathrm{dom}\mathrm{DProd}{s}\wedge {G}\mathrm{DProd}{s}={U}\right)$

Proof

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