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𝐺 )
Assertion pgp0 ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺s { 0 } ) )

Proof

Step Hyp Ref Expression
1 pgp0.1 0 = ( 0g𝐺 )
2 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
3 2 adantl ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℕ )
4 3 nncnd ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℂ )
5 4 exp0d ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ↑ 0 ) = 1 )
6 1 fvexi 0 ∈ V
7 hashsng ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
8 6 7 ax-mp ( ♯ ‘ { 0 } ) = 1
9 1 0subg ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
10 9 adantr ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
11 eqid ( 𝐺s { 0 } ) = ( 𝐺s { 0 } )
12 11 subgbas ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) → { 0 } = ( Base ‘ ( 𝐺s { 0 } ) ) )
13 10 12 syl ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → { 0 } = ( Base ‘ ( 𝐺s { 0 } ) ) )
14 13 fveq2d ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( ♯ ‘ { 0 } ) = ( ♯ ‘ ( Base ‘ ( 𝐺s { 0 } ) ) ) )
15 8 14 eqtr3id ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 1 = ( ♯ ‘ ( Base ‘ ( 𝐺s { 0 } ) ) ) )
16 5 15 eqtr2d ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( ♯ ‘ ( Base ‘ ( 𝐺s { 0 } ) ) ) = ( 𝑃 ↑ 0 ) )
17 11 subggrp ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺s { 0 } ) ∈ Grp )
18 10 17 syl ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( 𝐺s { 0 } ) ∈ Grp )
19 simpr ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 ∈ ℙ )
20 0nn0 0 ∈ ℕ0
21 20 a1i ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 0 ∈ ℕ0 )
22 eqid ( Base ‘ ( 𝐺s { 0 } ) ) = ( Base ‘ ( 𝐺s { 0 } ) )
23 22 pgpfi1 ( ( ( 𝐺s { 0 } ) ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 0 ∈ ℕ0 ) → ( ( ♯ ‘ ( Base ‘ ( 𝐺s { 0 } ) ) ) = ( 𝑃 ↑ 0 ) → 𝑃 pGrp ( 𝐺s { 0 } ) ) )
24 18 19 21 23 syl3anc ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → ( ( ♯ ‘ ( Base ‘ ( 𝐺s { 0 } ) ) ) = ( 𝑃 ↑ 0 ) → 𝑃 pGrp ( 𝐺s { 0 } ) ) )
25 16 24 mpd ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺s { 0 } ) )