Metamath Proof Explorer

Theorem pgp0

Description: The identity subgroup is a P -group for every prime P . (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis pgp0.1 
|- .0. = ( 0g ` G )
Assertion pgp0 
|- ( ( G e. Grp /\ P e. Prime ) -> P pGrp ( G |`s { .0. } ) )

Proof

Step Hyp Ref Expression
1 pgp0.1 
 |-  .0. = ( 0g ` G )
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 2 adantl 
 |-  ( ( G e. Grp /\ P e. Prime ) -> P e. NN )
4 3 nncnd 
 |-  ( ( G e. Grp /\ P e. Prime ) -> P e. CC )
5 4 exp0d 
 |-  ( ( G e. Grp /\ P e. Prime ) -> ( P ^ 0 ) = 1 )
6 1 fvexi 
 |-  .0. e. _V
7 hashsng 
 |-  ( .0. e. _V -> ( # ` { .0. } ) = 1 )
8 6 7 ax-mp 
 |-  ( # ` { .0. } ) = 1
9 1 0subg 
 |-  ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )
10 9 adantr 
 |-  ( ( G e. Grp /\ P e. Prime ) -> { .0. } e. ( SubGrp ` G ) )
11 eqid 
 |-  ( G |`s { .0. } ) = ( G |`s { .0. } )
12 11 subgbas 
 |-  ( { .0. } e. ( SubGrp ` G ) -> { .0. } = ( Base ` ( G |`s { .0. } ) ) )
13 10 12 syl 
 |-  ( ( G e. Grp /\ P e. Prime ) -> { .0. } = ( Base ` ( G |`s { .0. } ) ) )
14 13 fveq2d 
 |-  ( ( G e. Grp /\ P e. Prime ) -> ( # ` { .0. } ) = ( # ` ( Base ` ( G |`s { .0. } ) ) ) )
15 8 14 eqtr3id 
 |-  ( ( G e. Grp /\ P e. Prime ) -> 1 = ( # ` ( Base ` ( G |`s { .0. } ) ) ) )
16 5 15 eqtr2d 
 |-  ( ( G e. Grp /\ P e. Prime ) -> ( # ` ( Base ` ( G |`s { .0. } ) ) ) = ( P ^ 0 ) )
17 11 subggrp 
 |-  ( { .0. } e. ( SubGrp ` G ) -> ( G |`s { .0. } ) e. Grp )
18 10 17 syl 
 |-  ( ( G e. Grp /\ P e. Prime ) -> ( G |`s { .0. } ) e. Grp )
19 simpr 
 |-  ( ( G e. Grp /\ P e. Prime ) -> P e. Prime )
20 0nn0 
 |-  0 e. NN0
21 20 a1i 
 |-  ( ( G e. Grp /\ P e. Prime ) -> 0 e. NN0 )
22 eqid 
 |-  ( Base ` ( G |`s { .0. } ) ) = ( Base ` ( G |`s { .0. } ) )
23 22 pgpfi1 
 |-  ( ( ( G |`s { .0. } ) e. Grp /\ P e. Prime /\ 0 e. NN0 ) -> ( ( # ` ( Base ` ( G |`s { .0. } ) ) ) = ( P ^ 0 ) -> P pGrp ( G |`s { .0. } ) ) )
24 18 19 21 23 syl3anc 
 |-  ( ( G e. Grp /\ P e. Prime ) -> ( ( # ` ( Base ` ( G |`s { .0. } ) ) ) = ( P ^ 0 ) -> P pGrp ( G |`s { .0. } ) ) )
25 16 24 mpd 
 |-  ( ( G e. Grp /\ P e. Prime ) -> P pGrp ( G |`s { .0. } ) )