Metamath Proof Explorer

Theorem pgpfac1lem3a

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 4-Jun-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 )
pgpfac1.m 
|- ( ph -> M e. ZZ )
pgpfac1.mw 
|- ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )
Assertion pgpfac1lem3a 
|- ( ph -> ( P || E /\ P || M ) )

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 pgpfac1.m 
 |-  ( ph -> M e. ZZ )
21 pgpfac1.mw 
 |-  ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )
22 18 eldifbd 
 |-  ( ph -> -. C e. ( S .(+) W ) )
23 pgpprm 
 |-  ( P pGrp G -> P e. Prime )
24 8 23 syl 
 |-  ( ph -> P e. Prime )
25 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
26 9 25 syl 
 |-  ( ph -> G e. Grp )
27 3 5 gexcl2 
 |-  ( ( G e. Grp /\ B e. Fin ) -> E e. NN )
28 26 10 27 syl2anc 
 |-  ( ph -> E e. NN )
29 pceq0 
 |-  ( ( P e. Prime /\ E e. NN ) -> ( ( P pCnt E ) = 0 <-> -. P || E ) )
30 24 28 29 syl2anc 
 |-  ( ph -> ( ( P pCnt E ) = 0 <-> -. P || E ) )
31 oveq2 
 |-  ( ( P pCnt E ) = 0 -> ( P ^ ( P pCnt E ) ) = ( P ^ 0 ) )
32 30 31 syl6bir 
 |-  ( ph -> ( -. P || E -> ( P ^ ( P pCnt E ) ) = ( P ^ 0 ) ) )
33 3 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
34 26 33 syl 
 |-  ( ph -> B =/= (/) )
35 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
36 10 35 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
37 34 36 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
38 24 37 pccld 
 |-  ( ph -> ( P pCnt ( # ` B ) ) e. NN0 )
39 3 5 gexdvds3 
 |-  ( ( G e. Grp /\ B e. Fin ) -> E || ( # ` B ) )
40 26 10 39 syl2anc 
 |-  ( ph -> E || ( # ` B ) )
41 3 pgphash 
 |-  ( ( P pGrp G /\ B e. Fin ) -> ( # ` B ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
42 8 10 41 syl2anc 
 |-  ( ph -> ( # ` B ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
43 40 42 breqtrd 
 |-  ( ph -> E || ( P ^ ( P pCnt ( # ` B ) ) ) )
44 oveq2 
 |-  ( k = ( P pCnt ( # ` B ) ) -> ( P ^ k ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
45 44 breq2d 
 |-  ( k = ( P pCnt ( # ` B ) ) -> ( E || ( P ^ k ) <-> E || ( P ^ ( P pCnt ( # ` B ) ) ) ) )
46 45 rspcev 
 |-  ( ( ( P pCnt ( # ` B ) ) e. NN0 /\ E || ( P ^ ( P pCnt ( # ` B ) ) ) ) -> E. k e. NN0 E || ( P ^ k ) )
47 38 43 46 syl2anc 
 |-  ( ph -> E. k e. NN0 E || ( P ^ k ) )
48 pcprmpw2 
 |-  ( ( P e. Prime /\ E e. NN ) -> ( E. k e. NN0 E || ( P ^ k ) <-> E = ( P ^ ( P pCnt E ) ) ) )
49 24 28 48 syl2anc 
 |-  ( ph -> ( E. k e. NN0 E || ( P ^ k ) <-> E = ( P ^ ( P pCnt E ) ) ) )
50 47 49 mpbid 
 |-  ( ph -> E = ( P ^ ( P pCnt E ) ) )
51 50 eqcomd 
 |-  ( ph -> ( P ^ ( P pCnt E ) ) = E )
52 prmnn 
 |-  ( P e. Prime -> P e. NN )
53 24 52 syl 
 |-  ( ph -> P e. NN )
54 53 nncnd 
 |-  ( ph -> P e. CC )
55 54 exp0d 
 |-  ( ph -> ( P ^ 0 ) = 1 )
56 51 55 eqeq12d 
 |-  ( ph -> ( ( P ^ ( P pCnt E ) ) = ( P ^ 0 ) <-> E = 1 ) )
57 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
58 26 57 syl 
 |-  ( ph -> G e. Mnd )
59 3 5 gex1 
 |-  ( G e. Mnd -> ( E = 1 <-> B ~~ 1o ) )
60 58 59 syl 
 |-  ( ph -> ( E = 1 <-> B ~~ 1o ) )
61 56 60 bitrd 
 |-  ( ph -> ( ( P ^ ( P pCnt E ) ) = ( P ^ 0 ) <-> B ~~ 1o ) )
62 32 61 sylibd 
 |-  ( ph -> ( -. P || E -> B ~~ 1o ) )
63 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
64 26 63 syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( ACS ` B ) )
65 64 acsmred 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
66 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
67 12 66 syl 
 |-  ( ph -> U C_ B )
68 67 13 sseldd 
 |-  ( ph -> A e. B )
69 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
70 65 68 69 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
71 2 70 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
72 7 lsmsubg2 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
73 9 71 14 72 syl3anc 
 |-  ( ph -> ( S .(+) W ) e. ( SubGrp ` G ) )
74 6 subg0cl 
 |-  ( ( S .(+) W ) e. ( SubGrp ` G ) -> .0. e. ( S .(+) W ) )
75 73 74 syl 
 |-  ( ph -> .0. e. ( S .(+) W ) )
76 75 snssd 
 |-  ( ph -> { .0. } C_ ( S .(+) W ) )
77 76 adantr 
 |-  ( ( ph /\ B ~~ 1o ) -> { .0. } C_ ( S .(+) W ) )
78 18 eldifad 
 |-  ( ph -> C e. U )
79 67 78 sseldd 
 |-  ( ph -> C e. B )
80 79 adantr 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. B )
81 3 6 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
82 26 81 syl 
 |-  ( ph -> .0. e. B )
83 en1eqsn 
 |-  ( ( .0. e. B /\ B ~~ 1o ) -> B = { .0. } )
84 82 83 sylan 
 |-  ( ( ph /\ B ~~ 1o ) -> B = { .0. } )
85 80 84 eleqtrd 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. { .0. } )
86 77 85 sseldd 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. ( S .(+) W ) )
87 86 ex 
 |-  ( ph -> ( B ~~ 1o -> C e. ( S .(+) W ) ) )
88 62 87 syld 
 |-  ( ph -> ( -. P || E -> C e. ( S .(+) W ) ) )
89 22 88 mt3d 
 |-  ( ph -> P || E )
90 28 nncnd 
 |-  ( ph -> E e. CC )
91 53 nnne0d 
 |-  ( ph -> P =/= 0 )
92 90 54 91 divcan1d 
 |-  ( ph -> ( ( E / P ) x. P ) = E )
93 11 92 eqtr4d 
 |-  ( ph -> ( O ` A ) = ( ( E / P ) x. P ) )
94 nndivdvds 
 |-  ( ( E e. NN /\ P e. NN ) -> ( P || E <-> ( E / P ) e. NN ) )
95 28 53 94 syl2anc 
 |-  ( ph -> ( P || E <-> ( E / P ) e. NN ) )
96 89 95 mpbid 
 |-  ( ph -> ( E / P ) e. NN )
97 96 nnzd 
 |-  ( ph -> ( E / P ) e. ZZ )
98 97 20 zmulcld 
 |-  ( ph -> ( ( E / P ) x. M ) e. ZZ )
99 68 snssd 
 |-  ( ph -> { A } C_ B )
100 65 1 99 mrcssidd 
 |-  ( ph -> { A } C_ ( K ` { A } ) )
101 100 2 sseqtrrdi 
 |-  ( ph -> { A } C_ S )
102 snssg 
 |-  ( A e. U -> ( A e. S <-> { A } C_ S ) )
103 13 102 syl 
 |-  ( ph -> ( A e. S <-> { A } C_ S ) )
104 101 103 mpbird 
 |-  ( ph -> A e. S )
105 19 subgmulgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( ( E / P ) x. M ) e. ZZ /\ A e. S ) -> ( ( ( E / P ) x. M ) .x. A ) e. S )
106 71 98 104 105 syl3anc 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. S )
107 prmz 
 |-  ( P e. Prime -> P e. ZZ )
108 24 107 syl 
 |-  ( ph -> P e. ZZ )
109 3 19 mulgcl 
 |-  ( ( G e. Grp /\ P e. ZZ /\ C e. B ) -> ( P .x. C ) e. B )
110 26 108 79 109 syl3anc 
 |-  ( ph -> ( P .x. C ) e. B )
111 3 19 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ A e. B ) -> ( M .x. A ) e. B )
112 26 20 68 111 syl3anc 
 |-  ( ph -> ( M .x. A ) e. B )
113 eqid 
 |-  ( +g ` G ) = ( +g ` G )
114 3 19 113 mulgdi 
 |-  ( ( G e. Abel /\ ( ( E / P ) e. ZZ /\ ( P .x. C ) e. B /\ ( M .x. A ) e. B ) ) -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) = ( ( ( E / P ) .x. ( P .x. C ) ) ( +g ` G ) ( ( E / P ) .x. ( M .x. A ) ) ) )
115 9 97 110 112 114 syl13anc 
 |-  ( ph -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) = ( ( ( E / P ) .x. ( P .x. C ) ) ( +g ` G ) ( ( E / P ) .x. ( M .x. A ) ) ) )
116 92 oveq1d 
 |-  ( ph -> ( ( ( E / P ) x. P ) .x. C ) = ( E .x. C ) )
117 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( ( E / P ) e. ZZ /\ P e. ZZ /\ C e. B ) ) -> ( ( ( E / P ) x. P ) .x. C ) = ( ( E / P ) .x. ( P .x. C ) ) )
118 26 97 108 79 117 syl13anc 
 |-  ( ph -> ( ( ( E / P ) x. P ) .x. C ) = ( ( E / P ) .x. ( P .x. C ) ) )
119 3 5 19 6 gexid 
 |-  ( C e. B -> ( E .x. C ) = .0. )
120 79 119 syl 
 |-  ( ph -> ( E .x. C ) = .0. )
121 116 118 120 3eqtr3rd 
 |-  ( ph -> .0. = ( ( E / P ) .x. ( P .x. C ) ) )
122 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( ( E / P ) e. ZZ /\ M e. ZZ /\ A e. B ) ) -> ( ( ( E / P ) x. M ) .x. A ) = ( ( E / P ) .x. ( M .x. A ) ) )
123 26 97 20 68 122 syl13anc 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) = ( ( E / P ) .x. ( M .x. A ) ) )
124 121 123 oveq12d 
 |-  ( ph -> ( .0. ( +g ` G ) ( ( ( E / P ) x. M ) .x. A ) ) = ( ( ( E / P ) .x. ( P .x. C ) ) ( +g ` G ) ( ( E / P ) .x. ( M .x. A ) ) ) )
125 3 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
126 71 125 syl 
 |-  ( ph -> S C_ B )
127 126 106 sseldd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. B )
128 3 113 6 grplid 
 |-  ( ( G e. Grp /\ ( ( ( E / P ) x. M ) .x. A ) e. B ) -> ( .0. ( +g ` G ) ( ( ( E / P ) x. M ) .x. A ) ) = ( ( ( E / P ) x. M ) .x. A ) )
129 26 127 128 syl2anc 
 |-  ( ph -> ( .0. ( +g ` G ) ( ( ( E / P ) x. M ) .x. A ) ) = ( ( ( E / P ) x. M ) .x. A ) )
130 115 124 129 3eqtr2d 
 |-  ( ph -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) = ( ( ( E / P ) x. M ) .x. A ) )
131 19 subgmulgcl 
 |-  ( ( W e. ( SubGrp ` G ) /\ ( E / P ) e. ZZ /\ ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W ) -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) e. W )
132 14 97 21 131 syl3anc 
 |-  ( ph -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) e. W )
133 130 132 eqeltrrd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. W )
134 106 133 elind 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. ( S i^i W ) )
135 134 15 eleqtrd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. { .0. } )
136 elsni 
 |-  ( ( ( ( E / P ) x. M ) .x. A ) e. { .0. } -> ( ( ( E / P ) x. M ) .x. A ) = .0. )
137 135 136 syl 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) = .0. )
138 3 4 19 6 oddvds 
 |-  ( ( G e. Grp /\ A e. B /\ ( ( E / P ) x. M ) e. ZZ ) -> ( ( O ` A ) || ( ( E / P ) x. M ) <-> ( ( ( E / P ) x. M ) .x. A ) = .0. ) )
139 26 68 98 138 syl3anc 
 |-  ( ph -> ( ( O ` A ) || ( ( E / P ) x. M ) <-> ( ( ( E / P ) x. M ) .x. A ) = .0. ) )
140 137 139 mpbird 
 |-  ( ph -> ( O ` A ) || ( ( E / P ) x. M ) )
141 93 140 eqbrtrrd 
 |-  ( ph -> ( ( E / P ) x. P ) || ( ( E / P ) x. M ) )
142 96 nnne0d 
 |-  ( ph -> ( E / P ) =/= 0 )
143 dvdscmulr 
 |-  ( ( P e. ZZ /\ M e. ZZ /\ ( ( E / P ) e. ZZ /\ ( E / P ) =/= 0 ) ) -> ( ( ( E / P ) x. P ) || ( ( E / P ) x. M ) <-> P || M ) )
144 108 20 97 142 143 syl112anc 
 |-  ( ph -> ( ( ( E / P ) x. P ) || ( ( E / P ) x. M ) <-> P || M ) )
145 141 144 mpbid 
 |-  ( ph -> P || M )
146 89 145 jca 
 |-  ( ph -> ( P || E /\ P || M ) )