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 ˙