MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pgpfac1lem5 Structured version   Visualization version   GIF version

Theorem pgpfac1lem5 19200
Description: Lemma for pgpfac1 19201. (Contributed by Mario Carneiro, 27-Apr-2016.)
Hypotheses
Ref Expression
pgpfac1.k 𝐾 = (mrCls‘(SubGrp‘𝐺))
pgpfac1.s 𝑆 = (𝐾‘{𝐴})
pgpfac1.b 𝐵 = (Base‘𝐺)
pgpfac1.o 𝑂 = (od‘𝐺)
pgpfac1.e 𝐸 = (gEx‘𝐺)
pgpfac1.z 0 = (0g𝐺)
pgpfac1.l = (LSSum‘𝐺)
pgpfac1.p (𝜑𝑃 pGrp 𝐺)
pgpfac1.g (𝜑𝐺 ∈ Abel)
pgpfac1.n (𝜑𝐵 ∈ Fin)
pgpfac1.oe (𝜑 → (𝑂𝐴) = 𝐸)
pgpfac1.u (𝜑𝑈 ∈ (SubGrp‘𝐺))
pgpfac1.au (𝜑𝐴𝑈)
pgpfac1.3 (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠𝑈𝐴𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠)))
Assertion
Ref Expression
pgpfac1lem5 (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
Distinct variable groups:   𝑡,𝑠, 0   𝐴,𝑠,𝑡   ,𝑠,𝑡   𝑃,𝑠,𝑡   𝐵,𝑠,𝑡   𝐺,𝑠,𝑡   𝑈,𝑠,𝑡   𝑆,𝑠,𝑡   𝜑,𝑠,𝑡   𝐾,𝑠,𝑡
Allowed substitution hints:   𝐸(𝑡,𝑠)   𝑂(𝑡,𝑠)

Proof of Theorem pgpfac1lem5
Dummy variables 𝑏 𝑢 𝑣 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pgpfac1.n . . . . . . . . . 10 (𝜑𝐵 ∈ Fin)
2 pwfi 8818 . . . . . . . . . 10 (𝐵 ∈ Fin ↔ 𝒫 𝐵 ∈ Fin)
31, 2sylib 220 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ Fin)
43adantr 483 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝒫 𝐵 ∈ Fin)
5 pgpfac1.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
65subgss 18279 . . . . . . . . . . 11 (𝑣 ∈ (SubGrp‘𝐺) → 𝑣𝐵)
763ad2ant2 1130 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ 𝑣 ∈ (SubGrp‘𝐺) ∧ (𝑣𝑈𝐴𝑣)) → 𝑣𝐵)
8 velpw 4543 . . . . . . . . . 10 (𝑣 ∈ 𝒫 𝐵𝑣𝐵)
97, 8sylibr 236 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ 𝑣 ∈ (SubGrp‘𝐺) ∧ (𝑣𝑈𝐴𝑣)) → 𝑣 ∈ 𝒫 𝐵)
109rabssdv 4050 . . . . . . . 8 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ⊆ 𝒫 𝐵)
114, 10ssfid 8740 . . . . . . 7 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin)
12 finnum 9376 . . . . . . 7 ({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card)
1311, 12syl 17 . . . . . 6 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card)
14 pgpfac1.s . . . . . . . . . 10 𝑆 = (𝐾‘{𝐴})
15 pgpfac1.g . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Abel)
16 ablgrp 18910 . . . . . . . . . . . . 13 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
1715, 16syl 17 . . . . . . . . . . . 12 (𝜑𝐺 ∈ Grp)
185subgacs 18312 . . . . . . . . . . . 12 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘𝐵))
19 acsmre 16922 . . . . . . . . . . . 12 ((SubGrp‘𝐺) ∈ (ACS‘𝐵) → (SubGrp‘𝐺) ∈ (Moore‘𝐵))
2017, 18, 193syl 18 . . . . . . . . . . 11 (𝜑 → (SubGrp‘𝐺) ∈ (Moore‘𝐵))
21 pgpfac1.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (SubGrp‘𝐺))
225subgss 18279 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐺) → 𝑈𝐵)
2321, 22syl 17 . . . . . . . . . . . 12 (𝜑𝑈𝐵)
24 pgpfac1.au . . . . . . . . . . . 12 (𝜑𝐴𝑈)
2523, 24sseldd 3967 . . . . . . . . . . 11 (𝜑𝐴𝐵)
26 pgpfac1.k . . . . . . . . . . . 12 𝐾 = (mrCls‘(SubGrp‘𝐺))
2726mrcsncl 16882 . . . . . . . . . . 11 (((SubGrp‘𝐺) ∈ (Moore‘𝐵) ∧ 𝐴𝐵) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺))
2820, 25, 27syl2anc 586 . . . . . . . . . 10 (𝜑 → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺))
2914, 28eqeltrid 2917 . . . . . . . . 9 (𝜑𝑆 ∈ (SubGrp‘𝐺))
3029adantr 483 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝑆 ∈ (SubGrp‘𝐺))
31 simpr 487 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝑆𝑈)
3224snssd 4741 . . . . . . . . . . . . 13 (𝜑 → {𝐴} ⊆ 𝑈)
3332, 23sstrd 3976 . . . . . . . . . . . 12 (𝜑 → {𝐴} ⊆ 𝐵)
3420, 26, 33mrcssidd 16895 . . . . . . . . . . 11 (𝜑 → {𝐴} ⊆ (𝐾‘{𝐴}))
3534, 14sseqtrrdi 4017 . . . . . . . . . 10 (𝜑 → {𝐴} ⊆ 𝑆)
36 snssg 4716 . . . . . . . . . . 11 (𝐴𝐵 → (𝐴𝑆 ↔ {𝐴} ⊆ 𝑆))
3725, 36syl 17 . . . . . . . . . 10 (𝜑 → (𝐴𝑆 ↔ {𝐴} ⊆ 𝑆))
3835, 37mpbird 259 . . . . . . . . 9 (𝜑𝐴𝑆)
3938adantr 483 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝐴𝑆)
40 psseq1 4063 . . . . . . . . . 10 (𝑣 = 𝑆 → (𝑣𝑈𝑆𝑈))
41 eleq2 2901 . . . . . . . . . 10 (𝑣 = 𝑆 → (𝐴𝑣𝐴𝑆))
4240, 41anbi12d 632 . . . . . . . . 9 (𝑣 = 𝑆 → ((𝑣𝑈𝐴𝑣) ↔ (𝑆𝑈𝐴𝑆)))
4342rspcev 3622 . . . . . . . 8 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑆𝑈𝐴𝑆)) → ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
4430, 31, 39, 43syl12anc 834 . . . . . . 7 ((𝜑𝑆𝑈) → ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
45 rabn0 4338 . . . . . . 7 ({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
4644, 45sylibr 236 . . . . . 6 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅)
47 simpr1 1190 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})
48 simpr2 1191 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ≠ ∅)
4911adantr 483 . . . . . . . . . . 11 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin)
5049, 47ssfid 8740 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ∈ Fin)
51 simpr3 1192 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → [] Or 𝑢)
52 fin1a2lem10 9830 . . . . . . . . . 10 ((𝑢 ≠ ∅ ∧ 𝑢 ∈ Fin ∧ [] Or 𝑢) → 𝑢𝑢)
5348, 50, 51, 52syl3anc 1367 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢𝑢)
5447, 53sseldd 3967 . . . . . . . 8 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})
5554ex 415 . . . . . . 7 ((𝜑𝑆𝑈) → ((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}))
5655alrimiv 1924 . . . . . 6 ((𝜑𝑆𝑈) → ∀𝑢((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}))
57 zornn0g 9926 . . . . . 6 (({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card ∧ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅ ∧ ∀𝑢((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤)
5813, 46, 56, 57syl3anc 1367 . . . . 5 ((𝜑𝑆𝑈) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤)
59 psseq1 4063 . . . . . . . 8 (𝑣 = 𝑤 → (𝑣𝑈𝑤𝑈))
60 eleq2 2901 . . . . . . . 8 (𝑣 = 𝑤 → (𝐴𝑣𝐴𝑤))
6159, 60anbi12d 632 . . . . . . 7 (𝑣 = 𝑤 → ((𝑣𝑈𝐴𝑣) ↔ (𝑤𝑈𝐴𝑤)))
6261ralrab 3684 . . . . . 6 (∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤 ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6362rexbii 3247 . . . . 5 (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤 ↔ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6458, 63sylib 220 . . . 4 ((𝜑𝑆𝑈) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6564ex 415 . . 3 (𝜑 → (𝑆𝑈 → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
66 pgpfac1.3 . . . . 5 (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠𝑈𝐴𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠)))
67 psseq1 4063 . . . . . . 7 (𝑣 = 𝑠 → (𝑣𝑈𝑠𝑈))
68 eleq2 2901 . . . . . . 7 (𝑣 = 𝑠 → (𝐴𝑣𝐴𝑠))
6967, 68anbi12d 632 . . . . . 6 (𝑣 = 𝑠 → ((𝑣𝑈𝐴𝑣) ↔ (𝑠𝑈𝐴𝑠)))
7069ralrab 3684 . . . . 5 (∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠𝑈𝐴𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠)))
7166, 70sylibr 236 . . . 4 (𝜑 → ∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠))
72 r19.29 3254 . . . . 5 ((∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
7369elrab 3679 . . . . . . 7 (𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ↔ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠)))
74 ineq2 4182 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (𝑆𝑡) = (𝑆𝑣))
7574eqeq1d 2823 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((𝑆𝑡) = { 0 } ↔ (𝑆𝑣) = { 0 }))
76 oveq2 7163 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (𝑆 𝑡) = (𝑆 𝑣))
7776eqeq1d 2823 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((𝑆 𝑡) = 𝑠 ↔ (𝑆 𝑣) = 𝑠))
7875, 77anbi12d 632 . . . . . . . . . 10 (𝑡 = 𝑣 → (((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠)))
7978cbvrexvw 3450 . . . . . . . . 9 (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ∃𝑣 ∈ (SubGrp‘𝐺)((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠))
80 simprrl 779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → 𝑠𝑈)
8180ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → 𝑠𝑈)
82 simpr2 1191 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑆 𝑣) = 𝑠)
8382psseq1d 4068 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ((𝑆 𝑣) ⊊ 𝑈𝑠𝑈))
8481, 83mpbird 259 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑆 𝑣) ⊊ 𝑈)
85 pssdif 4325 . . . . . . . . . . . . . . 15 ((𝑆 𝑣) ⊊ 𝑈 → (𝑈 ∖ (𝑆 𝑣)) ≠ ∅)
86 n0 4309 . . . . . . . . . . . . . . 15 ((𝑈 ∖ (𝑆 𝑣)) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
8785, 86sylib 220 . . . . . . . . . . . . . 14 ((𝑆 𝑣) ⊊ 𝑈 → ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
8884, 87syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
89 pgpfac1.o . . . . . . . . . . . . . . . 16 𝑂 = (od‘𝐺)
90 pgpfac1.e . . . . . . . . . . . . . . . 16 𝐸 = (gEx‘𝐺)
91 pgpfac1.z . . . . . . . . . . . . . . . 16 0 = (0g𝐺)
92 pgpfac1.l . . . . . . . . . . . . . . . 16 = (LSSum‘𝐺)
93 pgpfac1.p . . . . . . . . . . . . . . . . 17 (𝜑𝑃 pGrp 𝐺)
9493ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑃 pGrp 𝐺)
9515ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐺 ∈ Abel)
961ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐵 ∈ Fin)
97 pgpfac1.oe . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑂𝐴) = 𝐸)
9897ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑂𝐴) = 𝐸)
9921ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑈 ∈ (SubGrp‘𝐺))
10024ad3antrrr 728 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐴𝑈)
101 simplr 767 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑣 ∈ (SubGrp‘𝐺))
102 simprl1 1214 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆𝑣) = { 0 })
10384adantrr 715 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) ⊊ 𝑈)
104103pssssd 4073 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) ⊆ 𝑈)
105 simprl3 1216 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
10682adantrr 715 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) = 𝑠)
107 psseq1 4063 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 𝑣) = 𝑠 → ((𝑆 𝑣) ⊊ 𝑦𝑠𝑦))
108107notbid 320 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 𝑣) = 𝑠 → (¬ (𝑆 𝑣) ⊊ 𝑦 ↔ ¬ 𝑠𝑦))
109108imbi2d 343 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 𝑣) = 𝑠 → (((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦)))
110109ralbidv 3197 . . . . . . . . . . . . . . . . . . 19 ((𝑆 𝑣) = 𝑠 → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦)))
111 psseq1 4063 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝑦𝑈𝑤𝑈))
112 eleq2 2901 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝐴𝑦𝐴𝑤))
113111, 112anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → ((𝑦𝑈𝐴𝑦) ↔ (𝑤𝑈𝐴𝑤)))
114 psseq2 4064 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝑠𝑦𝑠𝑤))
115114notbid 320 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → (¬ 𝑠𝑦 ↔ ¬ 𝑠𝑤))
116113, 115imbi12d 347 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑤 → (((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦) ↔ ((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
117116cbvralvw 3449 . . . . . . . . . . . . . . . . . . 19 (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
118110, 117syl6bb 289 . . . . . . . . . . . . . . . . . 18 ((𝑆 𝑣) = 𝑠 → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
119106, 118syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
120105, 119mpbird 259 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦))
121 simprr 771 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
122 eqid 2821 . . . . . . . . . . . . . . . 16 (.g𝐺) = (.g𝐺)
12326, 14, 5, 89, 90, 91, 92, 94, 95, 96, 98, 99, 100, 101, 102, 104, 120, 121, 122pgpfac1lem4 19199 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
124123expr 459 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
125124exlimdv 1930 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
12688, 125mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
1271263exp2 1350 . . . . . . . . . . 11 (((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) → ((𝑆𝑣) = { 0 } → ((𝑆 𝑣) = 𝑠 → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))))
128127impd 413 . . . . . . . . . 10 (((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) → (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
129128rexlimdva 3284 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → (∃𝑣 ∈ (SubGrp‘𝐺)((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
13079, 129syl5bi 244 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
131130impd 413 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → ((∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13273, 131sylan2b 595 . . . . . 6 ((𝜑𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}) → ((∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
133132rexlimdva 3284 . . . . 5 (𝜑 → (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13472, 133syl5 34 . . . 4 (𝜑 → ((∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13571, 134mpand 693 . . 3 (𝜑 → (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13665, 135syld 47 . 2 (𝜑 → (𝑆𝑈 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
137910subg 18303 . . . . . 6 (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
13817, 137syl 17 . . . . 5 (𝜑 → { 0 } ∈ (SubGrp‘𝐺))
139138adantr 483 . . . 4 ((𝜑𝑆 = 𝑈) → { 0 } ∈ (SubGrp‘𝐺))
14091subg0cl 18286 . . . . . . . 8 (𝑆 ∈ (SubGrp‘𝐺) → 0𝑆)
14129, 140syl 17 . . . . . . 7 (𝜑0𝑆)
142141snssd 4741 . . . . . 6 (𝜑 → { 0 } ⊆ 𝑆)
143142adantr 483 . . . . 5 ((𝜑𝑆 = 𝑈) → { 0 } ⊆ 𝑆)
144 sseqin2 4191 . . . . 5 ({ 0 } ⊆ 𝑆 ↔ (𝑆 ∩ { 0 }) = { 0 })
145143, 144sylib 220 . . . 4 ((𝜑𝑆 = 𝑈) → (𝑆 ∩ { 0 }) = { 0 })
14692lsmss2 18792 . . . . . . 7 ((𝑆 ∈ (SubGrp‘𝐺) ∧ { 0 } ∈ (SubGrp‘𝐺) ∧ { 0 } ⊆ 𝑆) → (𝑆 { 0 }) = 𝑆)
14729, 138, 142, 146syl3anc 1367 . . . . . 6 (𝜑 → (𝑆 { 0 }) = 𝑆)
148147eqeq1d 2823 . . . . 5 (𝜑 → ((𝑆 { 0 }) = 𝑈𝑆 = 𝑈))
149148biimpar 480 . . . 4 ((𝜑𝑆 = 𝑈) → (𝑆 { 0 }) = 𝑈)
150 ineq2 4182 . . . . . . 7 (𝑡 = { 0 } → (𝑆𝑡) = (𝑆 ∩ { 0 }))
151150eqeq1d 2823 . . . . . 6 (𝑡 = { 0 } → ((𝑆𝑡) = { 0 } ↔ (𝑆 ∩ { 0 }) = { 0 }))
152 oveq2 7163 . . . . . . 7 (𝑡 = { 0 } → (𝑆 𝑡) = (𝑆 { 0 }))
153152eqeq1d 2823 . . . . . 6 (𝑡 = { 0 } → ((𝑆 𝑡) = 𝑈 ↔ (𝑆 { 0 }) = 𝑈))
154151, 153anbi12d 632 . . . . 5 (𝑡 = { 0 } → (((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈) ↔ ((𝑆 ∩ { 0 }) = { 0 } ∧ (𝑆 { 0 }) = 𝑈)))
155154rspcev 3622 . . . 4 (({ 0 } ∈ (SubGrp‘𝐺) ∧ ((𝑆 ∩ { 0 }) = { 0 } ∧ (𝑆 { 0 }) = 𝑈)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
156139, 145, 149, 155syl12anc 834 . . 3 ((𝜑𝑆 = 𝑈) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
157156ex 415 . 2 (𝜑 → (𝑆 = 𝑈 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
15826mrcsscl 16890 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘𝐵) ∧ {𝐴} ⊆ 𝑈𝑈 ∈ (SubGrp‘𝐺)) → (𝐾‘{𝐴}) ⊆ 𝑈)
15920, 32, 21, 158syl3anc 1367 . . . 4 (𝜑 → (𝐾‘{𝐴}) ⊆ 𝑈)
16014, 159eqsstrid 4014 . . 3 (𝜑𝑆𝑈)
161 sspss 4075 . . 3 (𝑆𝑈 ↔ (𝑆𝑈𝑆 = 𝑈))
162160, 161sylib 220 . 2 (𝜑 → (𝑆𝑈𝑆 = 𝑈))
163136, 157, 162mpjaod 856 1 (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1083  wal 1531   = wceq 1533  wex 1776  wcel 2110  wne 3016  wral 3138  wrex 3139  {crab 3142  cdif 3932  cin 3934  wss 3935  wpss 3936  c0 4290  𝒫 cpw 4538  {csn 4566   cuni 4837   class class class wbr 5065   Or wor 5472  dom cdm 5554  cfv 6354  (class class class)co 7155   [] crpss 7447  Fincfn 8508  cardccrd 9363  Basecbs 16482  0gc0g 16712  Moorecmre 16852  mrClscmrc 16853  ACScacs 16855  Grpcgrp 18102  .gcmg 18223  SubGrpcsubg 18272  odcod 18651  gExcgex 18652   pGrp cpgp 18653  LSSumclsm 18758  Abelcabl 18906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-inf2 9103  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-iin 4921  df-disj 5031  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-rpss 7448  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-2o 8102  df-oadd 8105  df-omul 8106  df-er 8288  df-ec 8290  df-qs 8294  df-map 8407  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-sup 8905  df-inf 8906  df-oi 8973  df-dju 9329  df-card 9367  df-acn 9370  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11699  df-3 11700  df-n0 11897  df-xnn0 11967  df-z 11981  df-uz 12243  df-q 12348  df-rp 12389  df-fz 12892  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13429  df-fac 13633  df-bc 13662  df-hash 13690  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-sum 15042  df-dvds 15607  df-gcd 15843  df-prm 16015  df-pc 16173  df-ndx 16485  df-slot 16486  df-base 16488  df-sets 16489  df-ress 16490  df-plusg 16577  df-0g 16714  df-mre 16856  df-mrc 16857  df-acs 16859  df-mgm 17851  df-sgrp 17900  df-mnd 17911  df-submnd 17956  df-grp 18105  df-minusg 18106  df-sbg 18107  df-mulg 18224  df-subg 18275  df-eqg 18277  df-ga 18419  df-cntz 18446  df-od 18655  df-gex 18656  df-pgp 18657  df-lsm 18760  df-cmn 18907  df-abl 18908
This theorem is referenced by:  pgpfac1  19201
  Copyright terms: Public domain W3C validator