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 ⊢G∈Grp∧P∈ℙ→PpGrpG↾𝑠0˙

Proof

Step Hyp Ref Expression
1 pgp0.1 ⊢0˙=0G
2 prmnn ⊢P∈ℙ→P∈ℕ
3 2 adantl ⊢G∈Grp∧P∈ℙ→P∈ℕ
4 3 nncnd ⊢G∈Grp∧P∈ℙ→P∈ℂ
5 4 exp0d ⊢G∈Grp∧P∈ℙ→P0=1
6 1 fvexi ⊢0˙∈V
7 hashsng ⊢0˙∈V→0˙=1
8 6 7 ax-mp ⊢0˙=1
9 1 0subg ⊢G∈Grp→0˙∈SubGrp⁡G
10 9 adantr ⊢G∈Grp∧P∈ℙ→0˙∈SubGrp⁡G
11 eqid ⊢G↾𝑠0˙=G↾𝑠0˙
12 11 subgbas ⊢0˙∈SubGrp⁡G→0˙=BaseG↾𝑠0˙
13 10 12 syl ⊢G∈Grp∧P∈ℙ→0˙=BaseG↾𝑠0˙
14 13 fveq2d ⊢G∈Grp∧P∈ℙ→0˙=BaseG↾𝑠0˙
15 8 14 eqtr3id ⊢G∈Grp∧P∈ℙ→1=BaseG↾𝑠0˙
16 5 15 eqtr2d ⊢G∈Grp∧P∈ℙ→BaseG↾𝑠0˙=P0
17 11 subggrp ⊢0˙∈SubGrp⁡G→G↾𝑠0˙∈Grp
18 10 17 syl ⊢G∈Grp∧P∈ℙ→G↾𝑠0˙∈Grp
19 simpr ⊢G∈Grp∧P∈ℙ→P∈ℙ
20 0nn0 ⊢0∈ℕ0
21 20 a1i ⊢G∈Grp∧P∈ℙ→0∈ℕ0
22 eqid ⊢BaseG↾𝑠0˙=BaseG↾𝑠0˙
23 22 pgpfi1 ⊢G↾𝑠0˙∈Grp∧P∈ℙ∧0∈ℕ0→BaseG↾𝑠0˙=P0→PpGrpG↾𝑠0˙
24 18 19 21 23 syl3anc ⊢G∈Grp∧P∈ℙ→BaseG↾𝑠0˙=P0→PpGrpG↾𝑠0˙
25 16 24 mpd ⊢G∈Grp∧P∈ℙ→PpGrpG↾𝑠0˙