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 biimtrrdi 
 |-  ( 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 26 grpmndd 
 |-  ( ph -> G e. Mnd )
58 3 5 gex1 
 |-  ( G e. Mnd -> ( E = 1 <-> B ~~ 1o ) )
59 57 58 syl 
 |-  ( ph -> ( E = 1 <-> B ~~ 1o ) )
60 56 59 bitrd 
 |-  ( ph -> ( ( P ^ ( P pCnt E ) ) = ( P ^ 0 ) <-> B ~~ 1o ) )
61 32 60 sylibd 
 |-  ( ph -> ( -. P || E -> B ~~ 1o ) )
62 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
63 26 62 syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( ACS ` B ) )
64 63 acsmred 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
65 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
66 12 65 syl 
 |-  ( ph -> U C_ B )
67 66 13 sseldd 
 |-  ( ph -> A e. B )
68 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
69 64 67 68 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
70 2 69 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
71 7 lsmsubg2 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
72 9 70 14 71 syl3anc 
 |-  ( ph -> ( S .(+) W ) e. ( SubGrp ` G ) )
73 6 subg0cl 
 |-  ( ( S .(+) W ) e. ( SubGrp ` G ) -> .0. e. ( S .(+) W ) )
74 72 73 syl 
 |-  ( ph -> .0. e. ( S .(+) W ) )
75 74 snssd 
 |-  ( ph -> { .0. } C_ ( S .(+) W ) )
76 75 adantr 
 |-  ( ( ph /\ B ~~ 1o ) -> { .0. } C_ ( S .(+) W ) )
77 18 eldifad 
 |-  ( ph -> C e. U )
78 66 77 sseldd 
 |-  ( ph -> C e. B )
79 78 adantr 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. B )
80 3 6 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
81 26 80 syl 
 |-  ( ph -> .0. e. B )
82 en1eqsn 
 |-  ( ( .0. e. B /\ B ~~ 1o ) -> B = { .0. } )
83 81 82 sylan 
 |-  ( ( ph /\ B ~~ 1o ) -> B = { .0. } )
84 79 83 eleqtrd 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. { .0. } )
85 76 84 sseldd 
 |-  ( ( ph /\ B ~~ 1o ) -> C e. ( S .(+) W ) )
86 85 ex 
 |-  ( ph -> ( B ~~ 1o -> C e. ( S .(+) W ) ) )
87 61 86 syld 
 |-  ( ph -> ( -. P || E -> C e. ( S .(+) W ) ) )
88 22 87 mt3d 
 |-  ( ph -> P || E )
89 28 nncnd 
 |-  ( ph -> E e. CC )
90 53 nnne0d 
 |-  ( ph -> P =/= 0 )
91 89 54 90 divcan1d 
 |-  ( ph -> ( ( E / P ) x. P ) = E )
92 11 91 eqtr4d 
 |-  ( ph -> ( O ` A ) = ( ( E / P ) x. P ) )
93 nndivdvds 
 |-  ( ( E e. NN /\ P e. NN ) -> ( P || E <-> ( E / P ) e. NN ) )
94 28 53 93 syl2anc 
 |-  ( ph -> ( P || E <-> ( E / P ) e. NN ) )
95 88 94 mpbid 
 |-  ( ph -> ( E / P ) e. NN )
96 95 nnzd 
 |-  ( ph -> ( E / P ) e. ZZ )
97 96 20 zmulcld 
 |-  ( ph -> ( ( E / P ) x. M ) e. ZZ )
98 67 snssd 
 |-  ( ph -> { A } C_ B )
99 64 1 98 mrcssidd 
 |-  ( ph -> { A } C_ ( K ` { A } ) )
100 99 2 sseqtrrdi 
 |-  ( ph -> { A } C_ S )
101 snssg 
 |-  ( A e. U -> ( A e. S <-> { A } C_ S ) )
102 13 101 syl 
 |-  ( ph -> ( A e. S <-> { A } C_ S ) )
103 100 102 mpbird 
 |-  ( ph -> A e. S )
104 19 subgmulgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( ( E / P ) x. M ) e. ZZ /\ A e. S ) -> ( ( ( E / P ) x. M ) .x. A ) e. S )
105 70 97 103 104 syl3anc 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. S )
106 prmz 
 |-  ( P e. Prime -> P e. ZZ )
107 24 106 syl 
 |-  ( ph -> P e. ZZ )
108 3 19 mulgcl 
 |-  ( ( G e. Grp /\ P e. ZZ /\ C e. B ) -> ( P .x. C ) e. B )
109 26 107 78 108 syl3anc 
 |-  ( ph -> ( P .x. C ) e. B )
110 3 19 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ A e. B ) -> ( M .x. A ) e. B )
111 26 20 67 110 syl3anc 
 |-  ( ph -> ( M .x. A ) e. B )
112 eqid 
 |-  ( +g ` G ) = ( +g ` G )
113 3 19 112 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 ) ) ) )
114 9 96 109 111 113 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 ) ) ) )
115 91 oveq1d 
 |-  ( ph -> ( ( ( E / P ) x. P ) .x. C ) = ( E .x. C ) )
116 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 ) ) )
117 26 96 107 78 116 syl13anc 
 |-  ( ph -> ( ( ( E / P ) x. P ) .x. C ) = ( ( E / P ) .x. ( P .x. C ) ) )
118 3 5 19 6 gexid 
 |-  ( C e. B -> ( E .x. C ) = .0. )
119 78 118 syl 
 |-  ( ph -> ( E .x. C ) = .0. )
120 115 117 119 3eqtr3rd 
 |-  ( ph -> .0. = ( ( E / P ) .x. ( P .x. C ) ) )
121 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 ) ) )
122 26 96 20 67 121 syl13anc 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) = ( ( E / P ) .x. ( M .x. A ) ) )
123 120 122 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 ) ) ) )
124 3 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
125 70 124 syl 
 |-  ( ph -> S C_ B )
126 125 105 sseldd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. B )
127 3 112 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 ) )
128 26 126 127 syl2anc 
 |-  ( ph -> ( .0. ( +g ` G ) ( ( ( E / P ) x. M ) .x. A ) ) = ( ( ( E / P ) x. M ) .x. A ) )
129 114 123 128 3eqtr2d 
 |-  ( ph -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) = ( ( ( E / P ) x. M ) .x. A ) )
130 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 )
131 14 96 21 130 syl3anc 
 |-  ( ph -> ( ( E / P ) .x. ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) ) e. W )
132 129 131 eqeltrrd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. W )
133 105 132 elind 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. ( S i^i W ) )
134 133 15 eleqtrd 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) e. { .0. } )
135 elsni 
 |-  ( ( ( ( E / P ) x. M ) .x. A ) e. { .0. } -> ( ( ( E / P ) x. M ) .x. A ) = .0. )
136 134 135 syl 
 |-  ( ph -> ( ( ( E / P ) x. M ) .x. A ) = .0. )
137 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. ) )
138 26 67 97 137 syl3anc 
 |-  ( ph -> ( ( O ` A ) || ( ( E / P ) x. M ) <-> ( ( ( E / P ) x. M ) .x. A ) = .0. ) )
139 136 138 mpbird 
 |-  ( ph -> ( O ` A ) || ( ( E / P ) x. M ) )
140 92 139 eqbrtrrd 
 |-  ( ph -> ( ( E / P ) x. P ) || ( ( E / P ) x. M ) )
141 95 nnne0d 
 |-  ( ph -> ( E / P ) =/= 0 )
142 dvdscmulr 
 |-  ( ( P e. ZZ /\ M e. ZZ /\ ( ( E / P ) e. ZZ /\ ( E / P ) =/= 0 ) ) -> ( ( ( E / P ) x. P ) || ( ( E / P ) x. M ) <-> P || M ) )
143 107 20 96 141 142 syl112anc 
 |-  ( ph -> ( ( ( E / P ) x. P ) || ( ( E / P ) x. M ) <-> P || M ) )
144 140 143 mpbid 
 |-  ( ph -> P || M )
145 88 144 jca 
 |-  ( ph -> ( P || E /\ P || M ) )