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. = ( 0g ` G )
pgpfac1.l 
|- .(+) = ( LSSum ` G )
pgpfac1.p 
|- ( ph -> P pGrp G )
pgpfac1.g 
|- ( ph -> G e. Abel )
pgpfac1.n 
|- ( ph -> B e. Fin )
pgpfac1.oe 
|- ( ph -> ( O ` A ) = E )
pgpfac1.u 
|- ( ph -> U e. ( SubGrp ` G ) )
pgpfac1.au 
|- ( ph -> A e. U )
pgpfac1.w 
|- ( ph -> W e. ( SubGrp ` G ) )
pgpfac1.i 
|- ( ph -> ( S i^i W ) = { .0. } )
pgpfac1.ss 
|- ( ph -> ( S .(+) W ) C_ U )
pgpfac1.2 
|- ( ph -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
Assertion pgpfac1lem1 
|- ( ( ph /\ C e. ( 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. = ( 0g ` G )
7 pgpfac1.l 
 |-  .(+) = ( LSSum ` G )
8 pgpfac1.p 
 |-  ( ph -> P pGrp G )
9 pgpfac1.g 
 |-  ( ph -> G e. Abel )
10 pgpfac1.n 
 |-  ( ph -> B e. Fin )
11 pgpfac1.oe 
 |-  ( ph -> ( O ` A ) = E )
12 pgpfac1.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
13 pgpfac1.au 
 |-  ( ph -> A e. U )
14 pgpfac1.w 
 |-  ( ph -> W e. ( SubGrp ` G ) )
15 pgpfac1.i 
 |-  ( ph -> ( S i^i W ) = { .0. } )
16 pgpfac1.ss 
 |-  ( ph -> ( S .(+) W ) C_ U )
17 pgpfac1.2 
 |-  ( ph -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
18 16 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( S .(+) W ) C_ U )
19 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
20 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
21 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` B ) -> ( SubGrp ` G ) e. ( Moore ` B ) )
22 9 19 20 21 4syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
23 22 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( SubGrp ` G ) e. ( Moore ` B ) )
24 eldifi 
 |-  ( C e. ( U \ ( S .(+) W ) ) -> C e. U )
25 24 adantl 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> C e. U )
26 25 snssd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> { C } C_ U )
27 12 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> U e. ( SubGrp ` G ) )
28 1 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ { C } C_ U /\ U e. ( SubGrp ` G ) ) -> ( K ` { C } ) C_ U )
29 23 26 27 28 syl3anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( K ` { C } ) C_ U )
30 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
31 12 30 syl 
 |-  ( ph -> U C_ B )
32 31 13 sseldd 
 |-  ( ph -> A e. B )
33 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
34 22 32 33 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
35 2 34 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
36 7 lsmsubg2 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
37 9 35 14 36 syl3anc 
 |-  ( ph -> ( S .(+) W ) e. ( SubGrp ` G ) )
38 37 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
39 31 sselda 
 |-  ( ( ph /\ C e. U ) -> C e. B )
40 24 39 sylan2 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> C e. B )
41 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ C e. B ) -> ( K ` { C } ) e. ( SubGrp ` G ) )
42 23 40 41 syl2anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( K ` { C } ) e. ( SubGrp ` G ) )
43 7 lsmlub 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ ( K ` { C } ) e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( ( ( S .(+) W ) C_ U /\ ( K ` { C } ) C_ U ) <-> ( ( S .(+) W ) .(+) ( K ` { C } ) ) C_ U ) )
44 38 42 27 43 syl3anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( ( S .(+) W ) C_ U /\ ( K ` { C } ) C_ U ) <-> ( ( S .(+) W ) .(+) ( K ` { C } ) ) C_ U ) )
45 18 29 44 mpbi2and 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) C_ U )
46 7 lsmub1 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ ( K ` { C } ) e. ( SubGrp ` G ) ) -> ( S .(+) W ) C_ ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
47 38 42 46 syl2anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( S .(+) W ) C_ ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
48 7 lsmub2 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ ( K ` { C } ) e. ( SubGrp ` G ) ) -> ( K ` { C } ) C_ ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
49 38 42 48 syl2anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( K ` { C } ) C_ ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
50 40 snssd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> { C } C_ B )
51 23 1 50 mrcssidd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> { C } C_ ( K ` { C } ) )
52 snssg 
 |-  ( C e. B -> ( C e. ( K ` { C } ) <-> { C } C_ ( K ` { C } ) ) )
53 40 52 syl 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( C e. ( K ` { C } ) <-> { C } C_ ( K ` { C } ) ) )
54 51 53 mpbird 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> C e. ( K ` { C } ) )
55 49 54 sseldd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> C e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
56 eldifn 
 |-  ( C e. ( U \ ( S .(+) W ) ) -> -. C e. ( S .(+) W ) )
57 56 adantl 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> -. C e. ( S .(+) W ) )
58 47 55 57 ssnelpssd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
59 7 lsmub1 
 |-  ( ( S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> S C_ ( S .(+) W ) )
60 35 14 59 syl2anc 
 |-  ( ph -> S C_ ( S .(+) W ) )
61 32 snssd 
 |-  ( ph -> { A } C_ B )
62 22 1 61 mrcssidd 
 |-  ( ph -> { A } C_ ( K ` { A } ) )
63 62 2 sseqtrrdi 
 |-  ( ph -> { A } C_ S )
64 snssg 
 |-  ( A e. U -> ( A e. S <-> { A } C_ S ) )
65 13 64 syl 
 |-  ( ph -> ( A e. S <-> { A } C_ S ) )
66 63 65 mpbird 
 |-  ( ph -> A e. S )
67 60 66 sseldd 
 |-  ( ph -> A e. ( S .(+) W ) )
68 67 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> A e. ( S .(+) W ) )
69 47 68 sseldd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> A e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) )
70 psseq1 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( w C. U <-> ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U ) )
71 eleq2 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( A e. w <-> A e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) )
72 70 71 anbi12d 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( ( w C. U /\ A e. w ) <-> ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U /\ A e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) ) )
73 psseq2 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( ( S .(+) W ) C. w <-> ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) )
74 73 notbid 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( -. ( S .(+) W ) C. w <-> -. ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) )
75 72 74 imbi12d 
 |-  ( w = ( ( S .(+) W ) .(+) ( K ` { C } ) ) -> ( ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) <-> ( ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U /\ A e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) -> -. ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) ) )
76 17 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
77 9 adantr 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> G e. Abel )
78 7 lsmsubg2 
 |-  ( ( G e. Abel /\ ( S .(+) W ) e. ( SubGrp ` G ) /\ ( K ` { C } ) e. ( SubGrp ` G ) ) -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) e. ( SubGrp ` G ) )
79 77 38 42 78 syl3anc 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) e. ( SubGrp ` G ) )
80 75 76 79 rspcdva 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U /\ A e. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) -> -. ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) )
81 69 80 mpan2d 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U -> -. ( S .(+) W ) C. ( ( S .(+) W ) .(+) ( K ` { C } ) ) ) )
82 58 81 mt2d 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> -. ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U )
83 npss 
 |-  ( -. ( ( S .(+) W ) .(+) ( K ` { C } ) ) C. U <-> ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C_ U -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) = U ) )
84 82 83 sylib 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( ( S .(+) W ) .(+) ( K ` { C } ) ) C_ U -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) = U ) )
85 45 84 mpd 
 |-  ( ( ph /\ C e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { C } ) ) = U )