Metamath Proof Explorer

Theorem pgpfac1lem1

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

Ref Expression
Hypotheses pgpfac1.k ⊢K=mrCls⁡SubGrp⁡G
pgpfac1.s ⊢S=K⁡A
pgpfac1.b ⊢B=BaseG
pgpfac1.o ⊢O=od⁡G
pgpfac1.e ⊢E=gEx⁡G
pgpfac1.z ⊢0˙=0G
pgpfac1.l ⊢⊕˙=LSSum⁡G
pgpfac1.p ⊢φ→PpGrpG
pgpfac1.g ⊢φ→G∈Abel
pgpfac1.n ⊢φ→B∈Fin
pgpfac1.oe ⊢φ→O⁡A=E
pgpfac1.u ⊢φ→U∈SubGrp⁡G
pgpfac1.au ⊢φ→A∈U
pgpfac1.w ⊢φ→W∈SubGrp⁡G
pgpfac1.i ⊢φ→S∩W=0˙
pgpfac1.ss ⊢φ→S⊕˙W⊆U
pgpfac1.2 ⊢φ→∀w∈SubGrp⁡Gw⊂U∧A∈w→¬S⊕˙W⊂w
Assertion pgpfac1lem1 ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C=U

Proof

Step Hyp Ref Expression
1 pgpfac1.k ⊢K=mrCls⁡SubGrp⁡G
2 pgpfac1.s ⊢S=K⁡A
3 pgpfac1.b ⊢B=BaseG
4 pgpfac1.o ⊢O=od⁡G
5 pgpfac1.e ⊢E=gEx⁡G
6 pgpfac1.z ⊢0˙=0G
7 pgpfac1.l ⊢⊕˙=LSSum⁡G
8 pgpfac1.p ⊢φ→PpGrpG
9 pgpfac1.g ⊢φ→G∈Abel
10 pgpfac1.n ⊢φ→B∈Fin
11 pgpfac1.oe ⊢φ→O⁡A=E
12 pgpfac1.u ⊢φ→U∈SubGrp⁡G
13 pgpfac1.au ⊢φ→A∈U
14 pgpfac1.w ⊢φ→W∈SubGrp⁡G
15 pgpfac1.i ⊢φ→S∩W=0˙
16 pgpfac1.ss ⊢φ→S⊕˙W⊆U
17 pgpfac1.2 ⊢φ→∀w∈SubGrp⁡Gw⊂U∧A∈w→¬S⊕˙W⊂w
18 16 adantr ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊆U
19 ablgrp ⊢G∈Abel→G∈Grp
20 3 subgacs ⊢G∈Grp→SubGrp⁡G∈ACS⁡B
21 acsmre ⊢SubGrp⁡G∈ACS⁡B→SubGrp⁡G∈Moore⁡B
22 9 19 20 21 4syl ⊢φ→SubGrp⁡G∈Moore⁡B
23 22 adantr ⊢φ∧C∈U∖S⊕˙W→SubGrp⁡G∈Moore⁡B
24 eldifi ⊢C∈U∖S⊕˙W→C∈U
25 24 adantl ⊢φ∧C∈U∖S⊕˙W→C∈U
26 25 snssd ⊢φ∧C∈U∖S⊕˙W→C⊆U
27 12 adantr ⊢φ∧C∈U∖S⊕˙W→U∈SubGrp⁡G
28 1 mrcsscl ⊢SubGrp⁡G∈Moore⁡B∧C⊆U∧U∈SubGrp⁡G→K⁡C⊆U
29 23 26 27 28 syl3anc ⊢φ∧C∈U∖S⊕˙W→K⁡C⊆U
30 3 subgss ⊢U∈SubGrp⁡G→U⊆B
31 12 30 syl ⊢φ→U⊆B
32 31 13 sseldd ⊢φ→A∈B
33 1 mrcsncl ⊢SubGrp⁡G∈Moore⁡B∧A∈B→K⁡A∈SubGrp⁡G
34 22 32 33 syl2anc ⊢φ→K⁡A∈SubGrp⁡G
35 2 34 eqeltrid ⊢φ→S∈SubGrp⁡G
36 7 lsmsubg2 ⊢G∈Abel∧S∈SubGrp⁡G∧W∈SubGrp⁡G→S⊕˙W∈SubGrp⁡G
37 9 35 14 36 syl3anc ⊢φ→S⊕˙W∈SubGrp⁡G
38 37 adantr ⊢φ∧C∈U∖S⊕˙W→S⊕˙W∈SubGrp⁡G
39 31 sselda ⊢φ∧C∈U→C∈B
40 24 39 sylan2 ⊢φ∧C∈U∖S⊕˙W→C∈B
41 1 mrcsncl ⊢SubGrp⁡G∈Moore⁡B∧C∈B→K⁡C∈SubGrp⁡G
42 23 40 41 syl2anc ⊢φ∧C∈U∖S⊕˙W→K⁡C∈SubGrp⁡G
43 7 lsmlub ⊢S⊕˙W∈SubGrp⁡G∧K⁡C∈SubGrp⁡G∧U∈SubGrp⁡G→S⊕˙W⊆U∧K⁡C⊆U↔S⊕˙W⊕˙K⁡C⊆U
44 38 42 27 43 syl3anc ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊆U∧K⁡C⊆U↔S⊕˙W⊕˙K⁡C⊆U
45 18 29 44 mpbi2and ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C⊆U
46 7 lsmub1 ⊢S⊕˙W∈SubGrp⁡G∧K⁡C∈SubGrp⁡G→S⊕˙W⊆S⊕˙W⊕˙K⁡C
47 38 42 46 syl2anc ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊆S⊕˙W⊕˙K⁡C
48 7 lsmub2 ⊢S⊕˙W∈SubGrp⁡G∧K⁡C∈SubGrp⁡G→K⁡C⊆S⊕˙W⊕˙K⁡C
49 38 42 48 syl2anc ⊢φ∧C∈U∖S⊕˙W→K⁡C⊆S⊕˙W⊕˙K⁡C
50 40 snssd ⊢φ∧C∈U∖S⊕˙W→C⊆B
51 23 1 50 mrcssidd ⊢φ∧C∈U∖S⊕˙W→C⊆K⁡C
52 snssg ⊢C∈B→C∈K⁡C↔C⊆K⁡C
53 40 52 syl ⊢φ∧C∈U∖S⊕˙W→C∈K⁡C↔C⊆K⁡C
54 51 53 mpbird ⊢φ∧C∈U∖S⊕˙W→C∈K⁡C
55 49 54 sseldd ⊢φ∧C∈U∖S⊕˙W→C∈S⊕˙W⊕˙K⁡C
56 eldifn ⊢C∈U∖S⊕˙W→¬C∈S⊕˙W
57 56 adantl ⊢φ∧C∈U∖S⊕˙W→¬C∈S⊕˙W
58 47 55 57 ssnelpssd ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊂S⊕˙W⊕˙K⁡C
59 7 lsmub1 ⊢S∈SubGrp⁡G∧W∈SubGrp⁡G→S⊆S⊕˙W
60 35 14 59 syl2anc ⊢φ→S⊆S⊕˙W
61 32 snssd ⊢φ→A⊆B
62 22 1 61 mrcssidd ⊢φ→A⊆K⁡A
63 62 2 sseqtrrdi ⊢φ→A⊆S
64 snssg ⊢A∈U→A∈S↔A⊆S
65 13 64 syl ⊢φ→A∈S↔A⊆S
66 63 65 mpbird ⊢φ→A∈S
67 60 66 sseldd ⊢φ→A∈S⊕˙W
68 67 adantr ⊢φ∧C∈U∖S⊕˙W→A∈S⊕˙W
69 47 68 sseldd ⊢φ∧C∈U∖S⊕˙W→A∈S⊕˙W⊕˙K⁡C
70 psseq1 ⊢w=S⊕˙W⊕˙K⁡C→w⊂U↔S⊕˙W⊕˙K⁡C⊂U
71 eleq2 ⊢w=S⊕˙W⊕˙K⁡C→A∈w↔A∈S⊕˙W⊕˙K⁡C
72 70 71 anbi12d ⊢w=S⊕˙W⊕˙K⁡C→w⊂U∧A∈w↔S⊕˙W⊕˙K⁡C⊂U∧A∈S⊕˙W⊕˙K⁡C
73 psseq2 ⊢w=S⊕˙W⊕˙K⁡C→S⊕˙W⊂w↔S⊕˙W⊂S⊕˙W⊕˙K⁡C
74 73 notbid ⊢w=S⊕˙W⊕˙K⁡C→¬S⊕˙W⊂w↔¬S⊕˙W⊂S⊕˙W⊕˙K⁡C
75 72 74 imbi12d ⊢w=S⊕˙W⊕˙K⁡C→w⊂U∧A∈w→¬S⊕˙W⊂w↔S⊕˙W⊕˙K⁡C⊂U∧A∈S⊕˙W⊕˙K⁡C→¬S⊕˙W⊂S⊕˙W⊕˙K⁡C
76 17 adantr ⊢φ∧C∈U∖S⊕˙W→∀w∈SubGrp⁡Gw⊂U∧A∈w→¬S⊕˙W⊂w
77 9 adantr ⊢φ∧C∈U∖S⊕˙W→G∈Abel
78 7 lsmsubg2 ⊢G∈Abel∧S⊕˙W∈SubGrp⁡G∧K⁡C∈SubGrp⁡G→S⊕˙W⊕˙K⁡C∈SubGrp⁡G
79 77 38 42 78 syl3anc ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C∈SubGrp⁡G
80 75 76 79 rspcdva ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C⊂U∧A∈S⊕˙W⊕˙K⁡C→¬S⊕˙W⊂S⊕˙W⊕˙K⁡C
81 69 80 mpan2d ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C⊂U→¬S⊕˙W⊂S⊕˙W⊕˙K⁡C
82 58 81 mt2d ⊢φ∧C∈U∖S⊕˙W→¬S⊕˙W⊕˙K⁡C⊂U
83 npss ⊢¬S⊕˙W⊕˙K⁡C⊂U↔S⊕˙W⊕˙K⁡C⊆U→S⊕˙W⊕˙K⁡C=U
84 82 83 sylib ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C⊆U→S⊕˙W⊕˙K⁡C=U
85 45 84 mpd ⊢φ∧C∈U∖S⊕˙W→S⊕˙W⊕˙K⁡C=U