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

Theorem pgpfac1lem5 18678
Description: Lemma for pgpfac1 18679. (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 8426 . . . . . . . . . 10 (𝐵 ∈ Fin ↔ 𝒫 𝐵 ∈ Fin)
31, 2sylib 208 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ Fin)
43adantr 472 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝒫 𝐵 ∈ Fin)
5 pgpfac1.b . . . . . . . . . . . 12 𝐵 = (Base‘𝐺)
65subgss 17796 . . . . . . . . . . 11 (𝑣 ∈ (SubGrp‘𝐺) → 𝑣𝐵)
763ad2ant2 1129 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ 𝑣 ∈ (SubGrp‘𝐺) ∧ (𝑣𝑈𝐴𝑣)) → 𝑣𝐵)
8 selpw 4309 . . . . . . . . . 10 (𝑣 ∈ 𝒫 𝐵𝑣𝐵)
97, 8sylibr 224 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ 𝑣 ∈ (SubGrp‘𝐺) ∧ (𝑣𝑈𝐴𝑣)) → 𝑣 ∈ 𝒫 𝐵)
109rabssdv 3823 . . . . . . . 8 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ⊆ 𝒫 𝐵)
11 ssfi 8345 . . . . . . . 8 ((𝒫 𝐵 ∈ Fin ∧ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ⊆ 𝒫 𝐵) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin)
124, 10, 11syl2anc 696 . . . . . . 7 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin)
13 finnum 8964 . . . . . . 7 ({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card)
1412, 13syl 17 . . . . . 6 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card)
15 pgpfac1.s . . . . . . . . . 10 𝑆 = (𝐾‘{𝐴})
16 pgpfac1.g . . . . . . . . . . . . 13 (𝜑𝐺 ∈ Abel)
17 ablgrp 18398 . . . . . . . . . . . . 13 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
1816, 17syl 17 . . . . . . . . . . . 12 (𝜑𝐺 ∈ Grp)
195subgacs 17830 . . . . . . . . . . . 12 (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘𝐵))
20 acsmre 16514 . . . . . . . . . . . 12 ((SubGrp‘𝐺) ∈ (ACS‘𝐵) → (SubGrp‘𝐺) ∈ (Moore‘𝐵))
2118, 19, 203syl 18 . . . . . . . . . . 11 (𝜑 → (SubGrp‘𝐺) ∈ (Moore‘𝐵))
22 pgpfac1.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (SubGrp‘𝐺))
235subgss 17796 . . . . . . . . . . . . 13 (𝑈 ∈ (SubGrp‘𝐺) → 𝑈𝐵)
2422, 23syl 17 . . . . . . . . . . . 12 (𝜑𝑈𝐵)
25 pgpfac1.au . . . . . . . . . . . 12 (𝜑𝐴𝑈)
2624, 25sseldd 3745 . . . . . . . . . . 11 (𝜑𝐴𝐵)
27 pgpfac1.k . . . . . . . . . . . 12 𝐾 = (mrCls‘(SubGrp‘𝐺))
2827mrcsncl 16474 . . . . . . . . . . 11 (((SubGrp‘𝐺) ∈ (Moore‘𝐵) ∧ 𝐴𝐵) → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺))
2921, 26, 28syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐾‘{𝐴}) ∈ (SubGrp‘𝐺))
3015, 29syl5eqel 2843 . . . . . . . . 9 (𝜑𝑆 ∈ (SubGrp‘𝐺))
3130adantr 472 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝑆 ∈ (SubGrp‘𝐺))
32 simpr 479 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝑆𝑈)
3325snssd 4485 . . . . . . . . . . . . 13 (𝜑 → {𝐴} ⊆ 𝑈)
3433, 24sstrd 3754 . . . . . . . . . . . 12 (𝜑 → {𝐴} ⊆ 𝐵)
3521, 27, 34mrcssidd 16487 . . . . . . . . . . 11 (𝜑 → {𝐴} ⊆ (𝐾‘{𝐴}))
3635, 15syl6sseqr 3793 . . . . . . . . . 10 (𝜑 → {𝐴} ⊆ 𝑆)
37 snssg 4459 . . . . . . . . . . 11 (𝐴𝐵 → (𝐴𝑆 ↔ {𝐴} ⊆ 𝑆))
3826, 37syl 17 . . . . . . . . . 10 (𝜑 → (𝐴𝑆 ↔ {𝐴} ⊆ 𝑆))
3936, 38mpbird 247 . . . . . . . . 9 (𝜑𝐴𝑆)
4039adantr 472 . . . . . . . 8 ((𝜑𝑆𝑈) → 𝐴𝑆)
41 psseq1 3836 . . . . . . . . . 10 (𝑣 = 𝑆 → (𝑣𝑈𝑆𝑈))
42 eleq2 2828 . . . . . . . . . 10 (𝑣 = 𝑆 → (𝐴𝑣𝐴𝑆))
4341, 42anbi12d 749 . . . . . . . . 9 (𝑣 = 𝑆 → ((𝑣𝑈𝐴𝑣) ↔ (𝑆𝑈𝐴𝑆)))
4443rspcev 3449 . . . . . . . 8 ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑆𝑈𝐴𝑆)) → ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
4531, 32, 40, 44syl12anc 1475 . . . . . . 7 ((𝜑𝑆𝑈) → ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
46 rabn0 4101 . . . . . . 7 ({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ (SubGrp‘𝐺)(𝑣𝑈𝐴𝑣))
4745, 46sylibr 224 . . . . . 6 ((𝜑𝑆𝑈) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅)
48 simpr1 1234 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})
49 simpr2 1236 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ≠ ∅)
5012adantr 472 . . . . . . . . . . 11 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin)
51 ssfi 8345 . . . . . . . . . . 11 (({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ Fin ∧ 𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}) → 𝑢 ∈ Fin)
5250, 48, 51syl2anc 696 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ∈ Fin)
53 simpr3 1238 . . . . . . . . . 10 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → [] Or 𝑢)
54 fin1a2lem10 9423 . . . . . . . . . 10 ((𝑢 ≠ ∅ ∧ 𝑢 ∈ Fin ∧ [] Or 𝑢) → 𝑢𝑢)
5549, 52, 53, 54syl3anc 1477 . . . . . . . . 9 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢𝑢)
5648, 55sseldd 3745 . . . . . . . 8 (((𝜑𝑆𝑈) ∧ (𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢)) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})
5756ex 449 . . . . . . 7 ((𝜑𝑆𝑈) → ((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}))
5857alrimiv 2004 . . . . . 6 ((𝜑𝑆𝑈) → ∀𝑢((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}))
59 zornn0g 9519 . . . . . 6 (({𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∈ dom card ∧ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ≠ ∅ ∧ ∀𝑢((𝑢 ⊆ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ∧ 𝑢 ≠ ∅ ∧ [] Or 𝑢) → 𝑢 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)})) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤)
6014, 47, 58, 59syl3anc 1477 . . . . 5 ((𝜑𝑆𝑈) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤)
61 psseq1 3836 . . . . . . . 8 (𝑣 = 𝑤 → (𝑣𝑈𝑤𝑈))
62 eleq2 2828 . . . . . . . 8 (𝑣 = 𝑤 → (𝐴𝑣𝐴𝑤))
6361, 62anbi12d 749 . . . . . . 7 (𝑣 = 𝑤 → ((𝑣𝑈𝐴𝑣) ↔ (𝑤𝑈𝐴𝑤)))
6463ralrab 3509 . . . . . 6 (∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤 ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6564rexbii 3179 . . . . 5 (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ¬ 𝑠𝑤 ↔ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6660, 65sylib 208 . . . 4 ((𝜑𝑆𝑈) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
6766ex 449 . . 3 (𝜑 → (𝑆𝑈 → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
68 pgpfac1.3 . . . . 5 (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠𝑈𝐴𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠)))
69 psseq1 3836 . . . . . . 7 (𝑣 = 𝑠 → (𝑣𝑈𝑠𝑈))
70 eleq2 2828 . . . . . . 7 (𝑣 = 𝑠 → (𝐴𝑣𝐴𝑠))
7169, 70anbi12d 749 . . . . . 6 (𝑣 = 𝑠 → ((𝑣𝑈𝐴𝑣) ↔ (𝑠𝑈𝐴𝑠)))
7271ralrab 3509 . . . . 5 (∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠𝑈𝐴𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠)))
7368, 72sylibr 224 . . . 4 (𝜑 → ∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠))
74 r19.29 3210 . . . . 5 ((∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
7571elrab 3504 . . . . . . 7 (𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} ↔ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠)))
76 ineq2 3951 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (𝑆𝑡) = (𝑆𝑣))
7776eqeq1d 2762 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((𝑆𝑡) = { 0 } ↔ (𝑆𝑣) = { 0 }))
78 oveq2 6821 . . . . . . . . . . . 12 (𝑡 = 𝑣 → (𝑆 𝑡) = (𝑆 𝑣))
7978eqeq1d 2762 . . . . . . . . . . 11 (𝑡 = 𝑣 → ((𝑆 𝑡) = 𝑠 ↔ (𝑆 𝑣) = 𝑠))
8077, 79anbi12d 749 . . . . . . . . . 10 (𝑡 = 𝑣 → (((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠)))
8180cbvrexv 3311 . . . . . . . . 9 (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ↔ ∃𝑣 ∈ (SubGrp‘𝐺)((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠))
82 simprrl 823 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → 𝑠𝑈)
8382ad2antrr 764 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → 𝑠𝑈)
84 simpr2 1236 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑆 𝑣) = 𝑠)
8584psseq1d 3841 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ((𝑆 𝑣) ⊊ 𝑈𝑠𝑈))
8683, 85mpbird 247 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑆 𝑣) ⊊ 𝑈)
87 pssdif 4088 . . . . . . . . . . . . . . 15 ((𝑆 𝑣) ⊊ 𝑈 → (𝑈 ∖ (𝑆 𝑣)) ≠ ∅)
88 n0 4074 . . . . . . . . . . . . . . 15 ((𝑈 ∖ (𝑆 𝑣)) ≠ ∅ ↔ ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
8987, 88sylib 208 . . . . . . . . . . . . . 14 ((𝑆 𝑣) ⊊ 𝑈 → ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
9086, 89syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
91 pgpfac1.o . . . . . . . . . . . . . . . 16 𝑂 = (od‘𝐺)
92 pgpfac1.e . . . . . . . . . . . . . . . 16 𝐸 = (gEx‘𝐺)
93 pgpfac1.z . . . . . . . . . . . . . . . 16 0 = (0g𝐺)
94 pgpfac1.l . . . . . . . . . . . . . . . 16 = (LSSum‘𝐺)
95 pgpfac1.p . . . . . . . . . . . . . . . . 17 (𝜑𝑃 pGrp 𝐺)
9695ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑃 pGrp 𝐺)
9716ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐺 ∈ Abel)
981ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐵 ∈ Fin)
99 pgpfac1.oe . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑂𝐴) = 𝐸)
10099ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑂𝐴) = 𝐸)
10122ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑈 ∈ (SubGrp‘𝐺))
10225ad3antrrr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝐴𝑈)
103 simplr 809 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑣 ∈ (SubGrp‘𝐺))
104 simprl1 1267 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆𝑣) = { 0 })
10586adantrr 755 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) ⊊ 𝑈)
106105pssssd 3846 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) ⊆ 𝑈)
107 simprl3 1271 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
10884adantrr 755 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (𝑆 𝑣) = 𝑠)
109 psseq1 3836 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑆 𝑣) = 𝑠 → ((𝑆 𝑣) ⊊ 𝑦𝑠𝑦))
110109notbid 307 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 𝑣) = 𝑠 → (¬ (𝑆 𝑣) ⊊ 𝑦 ↔ ¬ 𝑠𝑦))
111110imbi2d 329 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 𝑣) = 𝑠 → (((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦)))
112111ralbidv 3124 . . . . . . . . . . . . . . . . . . 19 ((𝑆 𝑣) = 𝑠 → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦)))
113 psseq1 3836 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝑦𝑈𝑤𝑈))
114 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝐴𝑦𝐴𝑤))
115113, 114anbi12d 749 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → ((𝑦𝑈𝐴𝑦) ↔ (𝑤𝑈𝐴𝑤)))
116 psseq2 3837 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑤 → (𝑠𝑦𝑠𝑤))
117116notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑤 → (¬ 𝑠𝑦 ↔ ¬ 𝑠𝑤))
118115, 117imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑤 → (((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦) ↔ ((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
119118cbvralv 3310 . . . . . . . . . . . . . . . . . . 19 (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ 𝑠𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))
120112, 119syl6bb 276 . . . . . . . . . . . . . . . . . 18 ((𝑆 𝑣) = 𝑠 → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
121108, 120syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → (∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦) ↔ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)))
122107, 121mpbird 247 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∀𝑦 ∈ (SubGrp‘𝐺)((𝑦𝑈𝐴𝑦) → ¬ (𝑆 𝑣) ⊊ 𝑦))
123 simprr 813 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))
124 eqid 2760 . . . . . . . . . . . . . . . 16 (.g𝐺) = (.g𝐺)
12527, 15, 5, 91, 92, 93, 94, 96, 97, 98, 100, 101, 102, 103, 104, 106, 122, 123, 124pgpfac1lem4 18677 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) ∧ 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)))) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
126125expr 644 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
127126exlimdv 2010 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → (∃𝑏 𝑏 ∈ (𝑈 ∖ (𝑆 𝑣)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
12890, 127mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) ∧ ((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠 ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤))) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
1291283exp2 1448 . . . . . . . . . . 11 (((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) → ((𝑆𝑣) = { 0 } → ((𝑆 𝑣) = 𝑠 → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))))
130129impd 446 . . . . . . . . . 10 (((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) ∧ 𝑣 ∈ (SubGrp‘𝐺)) → (((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
131130rexlimdva 3169 . . . . . . . . 9 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → (∃𝑣 ∈ (SubGrp‘𝐺)((𝑆𝑣) = { 0 } ∧ (𝑆 𝑣) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
13281, 131syl5bi 232 . . . . . . . 8 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) → (∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))))
133132impd 446 . . . . . . 7 ((𝜑 ∧ (𝑠 ∈ (SubGrp‘𝐺) ∧ (𝑠𝑈𝐴𝑠))) → ((∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13475, 133sylan2b 493 . . . . . 6 ((𝜑𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}) → ((∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
135134rexlimdva 3169 . . . . 5 (𝜑 → (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)} (∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13674, 135syl5 34 . . . 4 (𝜑 → ((∀𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑠) ∧ ∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13773, 136mpand 713 . . 3 (𝜑 → (∃𝑠 ∈ {𝑣 ∈ (SubGrp‘𝐺) ∣ (𝑣𝑈𝐴𝑣)}∀𝑤 ∈ (SubGrp‘𝐺)((𝑤𝑈𝐴𝑤) → ¬ 𝑠𝑤) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
13867, 137syld 47 . 2 (𝜑 → (𝑆𝑈 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
139930subg 17820 . . . . . 6 (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
14018, 139syl 17 . . . . 5 (𝜑 → { 0 } ∈ (SubGrp‘𝐺))
141140adantr 472 . . . 4 ((𝜑𝑆 = 𝑈) → { 0 } ∈ (SubGrp‘𝐺))
14293subg0cl 17803 . . . . . . . 8 (𝑆 ∈ (SubGrp‘𝐺) → 0𝑆)
14330, 142syl 17 . . . . . . 7 (𝜑0𝑆)
144143snssd 4485 . . . . . 6 (𝜑 → { 0 } ⊆ 𝑆)
145144adantr 472 . . . . 5 ((𝜑𝑆 = 𝑈) → { 0 } ⊆ 𝑆)
146 sseqin2 3960 . . . . 5 ({ 0 } ⊆ 𝑆 ↔ (𝑆 ∩ { 0 }) = { 0 })
147145, 146sylib 208 . . . 4 ((𝜑𝑆 = 𝑈) → (𝑆 ∩ { 0 }) = { 0 })
14894lsmss2 18281 . . . . . . 7 ((𝑆 ∈ (SubGrp‘𝐺) ∧ { 0 } ∈ (SubGrp‘𝐺) ∧ { 0 } ⊆ 𝑆) → (𝑆 { 0 }) = 𝑆)
14930, 140, 144, 148syl3anc 1477 . . . . . 6 (𝜑 → (𝑆 { 0 }) = 𝑆)
150149eqeq1d 2762 . . . . 5 (𝜑 → ((𝑆 { 0 }) = 𝑈𝑆 = 𝑈))
151150biimpar 503 . . . 4 ((𝜑𝑆 = 𝑈) → (𝑆 { 0 }) = 𝑈)
152 ineq2 3951 . . . . . . 7 (𝑡 = { 0 } → (𝑆𝑡) = (𝑆 ∩ { 0 }))
153152eqeq1d 2762 . . . . . 6 (𝑡 = { 0 } → ((𝑆𝑡) = { 0 } ↔ (𝑆 ∩ { 0 }) = { 0 }))
154 oveq2 6821 . . . . . . 7 (𝑡 = { 0 } → (𝑆 𝑡) = (𝑆 { 0 }))
155154eqeq1d 2762 . . . . . 6 (𝑡 = { 0 } → ((𝑆 𝑡) = 𝑈 ↔ (𝑆 { 0 }) = 𝑈))
156153, 155anbi12d 749 . . . . 5 (𝑡 = { 0 } → (((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈) ↔ ((𝑆 ∩ { 0 }) = { 0 } ∧ (𝑆 { 0 }) = 𝑈)))
157156rspcev 3449 . . . 4 (({ 0 } ∈ (SubGrp‘𝐺) ∧ ((𝑆 ∩ { 0 }) = { 0 } ∧ (𝑆 { 0 }) = 𝑈)) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
158141, 147, 151, 157syl12anc 1475 . . 3 ((𝜑𝑆 = 𝑈) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
159158ex 449 . 2 (𝜑 → (𝑆 = 𝑈 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈)))
16027mrcsscl 16482 . . . . 5 (((SubGrp‘𝐺) ∈ (Moore‘𝐵) ∧ {𝐴} ⊆ 𝑈𝑈 ∈ (SubGrp‘𝐺)) → (𝐾‘{𝐴}) ⊆ 𝑈)
16121, 33, 22, 160syl3anc 1477 . . . 4 (𝜑 → (𝐾‘{𝐴}) ⊆ 𝑈)
16215, 161syl5eqss 3790 . . 3 (𝜑𝑆𝑈)
163 sspss 3848 . . 3 (𝑆𝑈 ↔ (𝑆𝑈𝑆 = 𝑈))
164162, 163sylib 208 . 2 (𝜑 → (𝑆𝑈𝑆 = 𝑈))
165138, 159, 164mpjaod 395 1 (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆𝑡) = { 0 } ∧ (𝑆 𝑡) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072  wal 1630   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  cdif 3712  cin 3714  wss 3715  wpss 3716  c0 4058  𝒫 cpw 4302  {csn 4321   cuni 4588   class class class wbr 4804   Or wor 5186  dom cdm 5266  cfv 6049  (class class class)co 6813   [] crpss 7101  Fincfn 8121  cardccrd 8951  Basecbs 16059  0gc0g 16302  Moorecmre 16444  mrClscmrc 16445  ACScacs 16447  Grpcgrp 17623  .gcmg 17741  SubGrpcsubg 17789  odcod 18144  gExcgex 18145   pGrp cpgp 18146  LSSumclsm 18249  Abelcabl 18394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-rpss 7102  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-omul 7734  df-er 7911  df-ec 7913  df-qs 7917  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-acn 8958  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-xnn0 11556  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-dvds 15183  df-gcd 15419  df-prm 15588  df-pc 15744  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-0g 16304  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-eqg 17794  df-ga 17923  df-cntz 17950  df-od 18148  df-gex 18149  df-pgp 18150  df-lsm 18251  df-cmn 18395  df-abl 18396
This theorem is referenced by:  pgpfac1  18679
  Copyright terms: Public domain W3C validator