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 )