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 = Base G
pgpfac1.o ⊢ O = od ⁡ G
pgpfac1.e ⊢ E = gEx ⁡ G
pgpfac1.z ⊢ 0 ˙ = 0 G
pgpfac1.l ⊢ ⊕ ˙ = LSSum ⁡ G
pgpfac1.p ⊢ φ → P pGrp G
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 ⁡ G w ⊂ 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 = Base G
4 pgpfac1.o ⊢ O = od ⁡ G
5 pgpfac1.e ⊢ E = gEx ⁡ G
6 pgpfac1.z ⊢ 0 ˙ = 0 G
7 pgpfac1.l ⊢ ⊕ ˙ = LSSum ⁡ G
8 pgpfac1.p ⊢ φ → P pGrp G
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 ⁡ G w ⊂ 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 ⁡ G w ⊂ 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