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 22 24 raleqtrdv 
 |-  ( ( 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 ) )
26 eqid 
 |-  ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
27 26 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 ) ) )
28 2 5 25 27 syl3anbrc 
 |-  ( ( P pGrp G /\ S e. ( SubGrp ` G ) ) -> P pGrp ( G |`s S ) )