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	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 𝑃 pGrp ( 𝐺 ↾_s { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		pgp0.1	⊢ 0 = ( 0_g ‘ 𝐺 )
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 ∈ ℕ₀
21	20	a1i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ) → 0 ∈ ℕ₀ )
22		eqid	⊢ ( Base ‘ ( 𝐺 ↾_s { 0 } ) ) = ( Base ‘ ( 𝐺 ↾_s { 0 } ) )
23	22	pgpfi1	⊢ ( ( ( 𝐺 ↾_s { 0 } ) ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 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 } ) )

Metamath Proof Explorer

Theorem pgp0

Proof