Metamath Proof Explorer

Theorem pgpfac1lem4

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 ) )
pgpfac1.c 
|- ( ph -> C e. ( U \ ( S .(+) W ) ) )
pgpfac1.mg 
|- .x. = ( .g ` G )
Assertion pgpfac1lem4 
|- ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = 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 pgpfac1.c 
 |-  ( ph -> C e. ( U \ ( S .(+) W ) ) )
19 pgpfac1.mg 
 |-  .x. = ( .g ` G )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 pgpfac1lem2 
 |-  ( ph -> ( P .x. C ) e. ( S .(+) W ) )
21 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
22 9 21 syl 
 |-  ( ph -> G e. Grp )
23 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
24 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` B ) -> ( SubGrp ` G ) e. ( Moore ` B ) )
25 22 23 24 3syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
26 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
27 12 26 syl 
 |-  ( ph -> U C_ B )
28 27 13 sseldd 
 |-  ( ph -> A e. B )
29 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
30 25 28 29 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
31 2 30 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
32 7 lsmcom 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) = ( W .(+) S ) )
33 9 31 14 32 syl3anc 
 |-  ( ph -> ( S .(+) W ) = ( W .(+) S ) )
34 20 33 eleqtrd 
 |-  ( ph -> ( P .x. C ) e. ( W .(+) S ) )
35 eqid 
 |-  ( -g ` G ) = ( -g ` G )
36 35 7 14 31 lsmelvalm 
 |-  ( ph -> ( ( P .x. C ) e. ( W .(+) S ) <-> E. w e. W E. s e. S ( P .x. C ) = ( w ( -g ` G ) s ) ) )
37 34 36 mpbid 
 |-  ( ph -> E. w e. W E. s e. S ( P .x. C ) = ( w ( -g ` G ) s ) )
38 eqid 
 |-  ( k e. ZZ |-> ( k .x. A ) ) = ( k e. ZZ |-> ( k .x. A ) )
39 3 19 38 1 cycsubg2 
 |-  ( ( G e. Grp /\ A e. B ) -> ( K ` { A } ) = ran ( k e. ZZ |-> ( k .x. A ) ) )
40 22 28 39 syl2anc 
 |-  ( ph -> ( K ` { A } ) = ran ( k e. ZZ |-> ( k .x. A ) ) )
41 2 40 syl5eq 
 |-  ( ph -> S = ran ( k e. ZZ |-> ( k .x. A ) ) )
42 41 rexeqdv 
 |-  ( ph -> ( E. s e. S ( P .x. C ) = ( w ( -g ` G ) s ) <-> E. s e. ran ( k e. ZZ |-> ( k .x. A ) ) ( P .x. C ) = ( w ( -g ` G ) s ) ) )
43 ovex 
 |-  ( k .x. A ) e. _V
44 43 rgenw 
 |-  A. k e. ZZ ( k .x. A ) e. _V
45 oveq2 
 |-  ( s = ( k .x. A ) -> ( w ( -g ` G ) s ) = ( w ( -g ` G ) ( k .x. A ) ) )
46 45 eqeq2d 
 |-  ( s = ( k .x. A ) -> ( ( P .x. C ) = ( w ( -g ` G ) s ) <-> ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) ) )
47 38 46 rexrnmptw 
 |-  ( A. k e. ZZ ( k .x. A ) e. _V -> ( E. s e. ran ( k e. ZZ |-> ( k .x. A ) ) ( P .x. C ) = ( w ( -g ` G ) s ) <-> E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) ) )
48 44 47 ax-mp 
 |-  ( E. s e. ran ( k e. ZZ |-> ( k .x. A ) ) ( P .x. C ) = ( w ( -g ` G ) s ) <-> E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) )
49 42 48 bitrdi 
 |-  ( ph -> ( E. s e. S ( P .x. C ) = ( w ( -g ` G ) s ) <-> E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) ) )
50 49 rexbidv 
 |-  ( ph -> ( E. w e. W E. s e. S ( P .x. C ) = ( w ( -g ` G ) s ) <-> E. w e. W E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) ) )
51 37 50 mpbid 
 |-  ( ph -> E. w e. W E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) )
52 rexcom 
 |-  ( E. w e. W E. k e. ZZ ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> E. k e. ZZ E. w e. W ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) )
53 51 52 sylib 
 |-  ( ph -> E. k e. ZZ E. w e. W ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) )
54 22 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> G e. Grp )
55 3 subgss 
 |-  ( W e. ( SubGrp ` G ) -> W C_ B )
56 14 55 syl 
 |-  ( ph -> W C_ B )
57 56 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> W C_ B )
58 57 sselda 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> w e. B )
59 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> k e. ZZ )
60 28 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> A e. B )
61 3 19 mulgcl 
 |-  ( ( G e. Grp /\ k e. ZZ /\ A e. B ) -> ( k .x. A ) e. B )
62 54 59 60 61 syl3anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> ( k .x. A ) e. B )
63 pgpprm 
 |-  ( P pGrp G -> P e. Prime )
64 prmz 
 |-  ( P e. Prime -> P e. ZZ )
65 8 63 64 3syl 
 |-  ( ph -> P e. ZZ )
66 18 eldifad 
 |-  ( ph -> C e. U )
67 27 66 sseldd 
 |-  ( ph -> C e. B )
68 3 19 mulgcl 
 |-  ( ( G e. Grp /\ P e. ZZ /\ C e. B ) -> ( P .x. C ) e. B )
69 22 65 67 68 syl3anc 
 |-  ( ph -> ( P .x. C ) e. B )
70 69 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> ( P .x. C ) e. B )
71 eqid 
 |-  ( +g ` G ) = ( +g ` G )
72 3 71 35 grpsubadd 
 |-  ( ( G e. Grp /\ ( w e. B /\ ( k .x. A ) e. B /\ ( P .x. C ) e. B ) ) -> ( ( w ( -g ` G ) ( k .x. A ) ) = ( P .x. C ) <-> ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) = w ) )
73 54 58 62 70 72 syl13anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> ( ( w ( -g ` G ) ( k .x. A ) ) = ( P .x. C ) <-> ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) = w ) )
74 eqcom 
 |-  ( ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> ( w ( -g ` G ) ( k .x. A ) ) = ( P .x. C ) )
75 eqcom 
 |-  ( w = ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) <-> ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) = w )
76 73 74 75 3bitr4g 
 |-  ( ( ( ph /\ k e. ZZ ) /\ w e. W ) -> ( ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> w = ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) ) )
77 76 rexbidva 
 |-  ( ( ph /\ k e. ZZ ) -> ( E. w e. W ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> E. w e. W w = ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) ) )
78 risset 
 |-  ( ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W <-> E. w e. W w = ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) )
79 77 78 bitr4di 
 |-  ( ( ph /\ k e. ZZ ) -> ( E. w e. W ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) )
80 79 rexbidva 
 |-  ( ph -> ( E. k e. ZZ E. w e. W ( P .x. C ) = ( w ( -g ` G ) ( k .x. A ) ) <-> E. k e. ZZ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) )
81 53 80 mpbid 
 |-  ( ph -> E. k e. ZZ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W )
82 8 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> P pGrp G )
83 9 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> G e. Abel )
84 10 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> B e. Fin )
85 11 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> ( O ` A ) = E )
86 12 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> U e. ( SubGrp ` G ) )
87 13 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> A e. U )
88 14 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> W e. ( SubGrp ` G ) )
89 15 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> ( S i^i W ) = { .0. } )
90 16 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> ( S .(+) W ) C_ U )
91 17 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
92 18 adantr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> C e. ( U \ ( S .(+) W ) ) )
93 simprl 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> k e. ZZ )
94 simprr 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W )
95 eqid 
 |-  ( C ( +g ` G ) ( ( k / P ) .x. A ) ) = ( C ( +g ` G ) ( ( k / P ) .x. A ) )
96 1 2 3 4 5 6 7 82 83 84 85 86 87 88 89 90 91 92 19 93 94 95 pgpfac1lem3 
 |-  ( ( ph /\ ( k e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( k .x. A ) ) e. W ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )
97 81 96 rexlimddv 
 |-  ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )