Metamath Proof Explorer


Theorem subgpgp

Description: A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Assertion subgpgp
|- ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> P pGrp ( G |`s S ) )

Proof

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 ) )