Metamath Proof Explorer

Theorem pgpfac1lem5

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses 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 pgpfac1lem5 ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 pgpfac1.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
2 pgpfac1.s ⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
3 pgpfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 pgpfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
5 pgpfac1.e ⊢ 𝐸 = ( gEx ‘ 𝐺 )
6 pgpfac1.z ⊢ 0 = ( 0g ‘ 𝐺 )
7 pgpfac1.l ⊢ ⊕ = ( LSSum ‘ 𝐺 )
8 pgpfac1.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
9 pgpfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
10 pgpfac1.n ⊢ ( 𝜑 → 𝐵 ∈ Fin )
11 pgpfac1.oe ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
12 pgpfac1.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
13 pgpfac1.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
14 pgpfac1.3 ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
15 pwfi ⊢ ( 𝐵 ∈ Fin ↔ 𝒫 𝐵 ∈ Fin )
16 10 15 sylib ⊢ ( 𝜑 → 𝒫 𝐵 ∈ Fin )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝒫 𝐵 ∈ Fin )
18 3 subgss ⊢ ( 𝑣 ∈ ( SubGrp ‘ 𝐺 ) → 𝑣 ⊆ 𝐵 )
19 18 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) → 𝑣 ⊆ 𝐵 )
20 velpw ⊢ ( 𝑣 ∈ 𝒫 𝐵 ↔ 𝑣 ⊆ 𝐵 )
21 19 20 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) → 𝑣 ∈ 𝒫 𝐵 )
22 21 rabssdv ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ⊆ 𝒫 𝐵 )
23 17 22 ssfid ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin )
24 finnum ⊢ ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card )
26 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
27 9 26 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
28 3 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
29 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
30 27 28 29 3syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
31 3 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
32 12 31 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
33 32 13 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
34 1 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
35 30 33 34 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
36 2 35 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝑆 ⊊ 𝑈 )
39 13 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑈 )
40 39 32 sstrd ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
41 30 1 40 mrcssidd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
42 41 2 sseqtrrdi ⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
43 snssg ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
44 33 43 syl ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
45 42 44 mpbird ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝐴 ∈ 𝑆 )
47 psseq1 ⊢ ( 𝑣 = 𝑆 → ( 𝑣 ⊊ 𝑈 ↔ 𝑆 ⊊ 𝑈 ) )
48 eleq2 ⊢ ( 𝑣 = 𝑆 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑆 ) )
49 47 48 anbi12d ⊢ ( 𝑣 = 𝑆 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑆 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑆 ) ) )
50 49 rspcev ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑆 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑆 ) ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) )
51 37 38 46 50 syl12anc ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) )
52 rabn0 ⊢ ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) )
53 51 52 sylibr ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ )
54 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } )
55 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ≠ ∅ )
56 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin )
57 56 54 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ∈ Fin )
58 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → [⊊] Or 𝑢 )
59 fin1a2lem10 ⊢ ( ( 𝑢 ≠ ∅ ∧ 𝑢 ∈ Fin ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ 𝑢 )
60 55 57 58 59 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → ∪ 𝑢 ∈ 𝑢 )
61 54 60 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } )
62 61 ex ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) )
63 62 alrimiv ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) )
64 zornn0g ⊢ ( ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card ∧ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ ∧ ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 )
65 25 53 63 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 )
66 psseq1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 ⊊ 𝑈 ↔ 𝑤 ⊊ 𝑈 ) )
67 eleq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑤 ) )
68 66 67 anbi12d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) ) )
69 68 ralrab ⊢ ( ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) )
70 69 rexbii ⊢ ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ↔ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) )
71 65 70 sylib ⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) )
72 71 ex ⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) )
73 psseq1 ⊢ ( 𝑣 = 𝑠 → ( 𝑣 ⊊ 𝑈 ↔ 𝑠 ⊊ 𝑈 ) )
74 eleq2 ⊢ ( 𝑣 = 𝑠 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑠 ) )
75 73 74 anbi12d ⊢ ( 𝑣 = 𝑠 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) )
76 75 ralrab ⊢ ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) )
77 14 76 sylibr ⊢ ( 𝜑 → ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) )
78 r19.29 ⊢ ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) )
79 75 elrab ⊢ ( 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) )
80 ineq2 ⊢ ( 𝑡 = 𝑣 → ( 𝑆 ∩ 𝑡 ) = ( 𝑆 ∩ 𝑣 ) )
81 80 eqeq1d ⊢ ( 𝑡 = 𝑣 → ( ( 𝑆 ∩ 𝑡 ) = { 0 } ↔ ( 𝑆 ∩ 𝑣 ) = { 0 } ) )
82 oveq2 ⊢ ( 𝑡 = 𝑣 → ( 𝑆 ⊕ 𝑡 ) = ( 𝑆 ⊕ 𝑣 ) )
83 82 eqeq1d ⊢ ( 𝑡 = 𝑣 → ( ( 𝑆 ⊕ 𝑡 ) = 𝑠 ↔ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) )
84 81 83 anbi12d ⊢ ( 𝑡 = 𝑣 → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) ) )
85 84 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) )
86 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → 𝑠 ⊊ 𝑈 )
87 86 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → 𝑠 ⊊ 𝑈 )
88 simpr2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑆 ⊕ 𝑣 ) = 𝑠 )
89 88 psseq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 ↔ 𝑠 ⊊ 𝑈 ) )
90 87 89 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 )
91 pssdif ⊢ ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 → ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ≠ ∅ )
92 n0 ⊢ ( ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) )
93 91 92 sylib ⊢ ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) )
94 90 93 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) )
95 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑃 pGrp 𝐺 )
96 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐺 ∈ Abel )
97 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐵 ∈ Fin )
98 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
99 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
100 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐴 ∈ 𝑈 )
101 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑣 ∈ ( SubGrp ‘ 𝐺 ) )
102 simprl1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ∩ 𝑣 ) = { 0 } )
103 90 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 )
104 103 pssssd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊆ 𝑈 )
105 simprl3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) )
106 88 adantrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) = 𝑠 )
107 psseq1 ⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ↔ 𝑠 ⊊ 𝑦 ) )
108 107 notbid ⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ↔ ¬ 𝑠 ⊊ 𝑦 ) )
109 108 imbi2d ⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ) )
110 109 ralbidv ⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ) )
111 psseq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ⊊ 𝑈 ↔ 𝑤 ⊊ 𝑈 ) )
112 eleq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑤 ) )
113 111 112 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) ↔ ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) ) )
114 psseq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑠 ⊊ 𝑦 ↔ 𝑠 ⊊ 𝑤 ) )
115 114 notbid ⊢ ( 𝑦 = 𝑤 → ( ¬ 𝑠 ⊊ 𝑦 ↔ ¬ 𝑠 ⊊ 𝑤 ) )
116 113 115 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ↔ ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) )
117 116 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) )
118 110 117 bitrdi ⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) )
119 106 118 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) )
120 105 119 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) )
121 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) )
122 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
123 1 2 3 4 5 6 7 95 96 97 98 99 100 101 102 104 120 121 122 pgpfac1lem4 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
124 123 expr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
125 124 exlimdv ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
126 94 125 mpd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
127 126 3exp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ∩ 𝑣 ) = { 0 } → ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) ) )
128 127 impd ⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) )
129 128 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) )
130 85 129 syl5bi ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) )
131 130 impd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
132 79 131 sylan2b ⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
133 132 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
134 78 133 syl5 ⊢ ( 𝜑 → ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
135 77 134 mpand ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
136 72 135 syld ⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
137 6 0subg ⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
138 27 137 syl ⊢ ( 𝜑 → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
140 6 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑆 )
141 36 140 syl ⊢ ( 𝜑 → 0 ∈ 𝑆 )
142 141 snssd ⊢ ( 𝜑 → { 0 } ⊆ 𝑆 )
143 142 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → { 0 } ⊆ 𝑆 )
144 sseqin2 ⊢ ( { 0 } ⊆ 𝑆 ↔ ( 𝑆 ∩ { 0 } ) = { 0 } )
145 143 144 sylib ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ( 𝑆 ∩ { 0 } ) = { 0 } )
146 7 lsmss2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ⊆ 𝑆 ) → ( 𝑆 ⊕ { 0 } ) = 𝑆 )
147 36 138 142 146 syl3anc ⊢ ( 𝜑 → ( 𝑆 ⊕ { 0 } ) = 𝑆 )
148 147 eqeq1d ⊢ ( 𝜑 → ( ( 𝑆 ⊕ { 0 } ) = 𝑈 ↔ 𝑆 = 𝑈 ) )
149 148 biimpar ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ( 𝑆 ⊕ { 0 } ) = 𝑈 )
150 ineq2 ⊢ ( 𝑡 = { 0 } → ( 𝑆 ∩ 𝑡 ) = ( 𝑆 ∩ { 0 } ) )
151 150 eqeq1d ⊢ ( 𝑡 = { 0 } → ( ( 𝑆 ∩ 𝑡 ) = { 0 } ↔ ( 𝑆 ∩ { 0 } ) = { 0 } ) )
152 oveq2 ⊢ ( 𝑡 = { 0 } → ( 𝑆 ⊕ 𝑡 ) = ( 𝑆 ⊕ { 0 } ) )
153 152 eqeq1d ⊢ ( 𝑡 = { 0 } → ( ( 𝑆 ⊕ 𝑡 ) = 𝑈 ↔ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) )
154 151 153 anbi12d ⊢ ( 𝑡 = { 0 } → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ↔ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) ) )
155 154 rspcev ⊢ ( ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
156 139 145 149 155 syl12anc ⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
157 156 ex ⊢ ( 𝜑 → ( 𝑆 = 𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) )
158 1 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ { 𝐴 } ⊆ 𝑈 ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 )
159 30 39 12 158 syl3anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 )
160 2 159 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ 𝑈 )
161 sspss ⊢ ( 𝑆 ⊆ 𝑈 ↔ ( 𝑆 ⊊ 𝑈 ∨ 𝑆 = 𝑈 ) )
162 160 161 sylib ⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 ∨ 𝑆 = 𝑈 ) )
163 136 157 162 mpjaod ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )