Step |
Hyp |
Ref |
Expression |
1 |
|
pgpprm |
|- ( P pGrp G -> P e. Prime ) |
2 |
1
|
adantr |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> P e. Prime ) |
3 |
|
eqid |
|- ( G |`s S ) = ( G |`s S ) |
4 |
3
|
subggrp |
|- ( S e. ( SubGrp ` G ) -> ( G |`s S ) e. Grp ) |
5 |
4
|
adantl |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> ( G |`s S ) e. Grp ) |
6 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
7 |
|
eqid |
|- ( od ` G ) = ( od ` G ) |
8 |
6 7
|
ispgp |
|- ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) ) |
9 |
8
|
simp3bi |
|- ( P pGrp G -> A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) |
10 |
9
|
adantr |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) |
11 |
6
|
subgss |
|- ( S e. ( SubGrp ` G ) -> S C_ ( Base ` G ) ) |
12 |
11
|
adantl |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> S C_ ( Base ` G ) ) |
13 |
|
ssralv |
|- ( S C_ ( Base ` G ) -> ( A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) -> A. x e. S E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) ) |
14 |
12 13
|
syl |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> ( A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) -> A. x e. S E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) ) |
15 |
|
eqid |
|- ( od ` ( G |`s S ) ) = ( od ` ( G |`s S ) ) |
16 |
3 7 15
|
subgod |
|- ( ( S e. ( SubGrp ` G ) /\ x e. S ) -> ( ( od ` G ) ` x ) = ( ( od ` ( G |`s S ) ) ` x ) ) |
17 |
16
|
adantll |
|- ( ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) /\ x e. S ) -> ( ( od ` G ) ` x ) = ( ( od ` ( G |`s S ) ) ` x ) ) |
18 |
17
|
eqeq1d |
|- ( ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) /\ x e. S ) -> ( ( ( od ` G ) ` x ) = ( P ^ n ) <-> ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
19 |
18
|
rexbidv |
|- ( ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) /\ x e. S ) -> ( E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) <-> E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
20 |
19
|
ralbidva |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> ( A. x e. S E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) <-> A. x e. S E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
21 |
14 20
|
sylibd |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> ( A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) -> A. x e. S E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
22 |
10 21
|
mpd |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> A. x e. S E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) |
23 |
3
|
subgbas |
|- ( S e. ( SubGrp ` G ) -> S = ( Base ` ( G |`s S ) ) ) |
24 |
23
|
adantl |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> S = ( Base ` ( G |`s S ) ) ) |
25 |
24
|
raleqdv |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> ( A. x e. S E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) <-> A. x e. ( Base ` ( G |`s S ) ) E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
26 |
22 25
|
mpbid |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> A. x e. ( Base ` ( G |`s S ) ) E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) |
27 |
|
eqid |
|- ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) ) |
28 |
27 15
|
ispgp |
|- ( P pGrp ( G |`s S ) <-> ( P e. Prime /\ ( G |`s S ) e. Grp /\ A. x e. ( Base ` ( G |`s S ) ) E. n e. NN0 ( ( od ` ( G |`s S ) ) ` x ) = ( P ^ n ) ) ) |
29 |
2 5 26 28
|
syl3anbrc |
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> P pGrp ( G |`s S ) ) |