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 } ) ) |