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 ˙ = 0 G
Assertion pgp0 G Grp P P pGrp G 𝑠 0 ˙

Proof

Step Hyp Ref Expression
1 pgp0.1 0 ˙ = 0 G
2 prmnn P P
3 2 adantl G Grp P P
4 3 nncnd G Grp P P
5 4 exp0d G Grp P P 0 = 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 ˙ = Base G 𝑠 0 ˙
13 10 12 syl G Grp P 0 ˙ = Base G 𝑠 0 ˙
14 13 fveq2d G Grp P 0 ˙ = Base G 𝑠 0 ˙
15 8 14 eqtr3id G Grp P 1 = Base G 𝑠 0 ˙
16 5 15 eqtr2d G Grp P Base G 𝑠 0 ˙ = P 0
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 Base G 𝑠 0 ˙ = Base G 𝑠 0 ˙
23 22 pgpfi1 G 𝑠 0 ˙ Grp P 0 0 Base G 𝑠 0 ˙ = P 0 P pGrp G 𝑠 0 ˙
24 18 19 21 23 syl3anc G Grp P Base G 𝑠 0 ˙ = P 0 P pGrp G 𝑠 0 ˙
25 16 24 mpd G Grp P P pGrp G 𝑠 0 ˙