| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fislw.1 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
| 2 |
|
slwhash.3 |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
| 3 |
|
slwhash.4 |
⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) |
| 4 |
|
slwsubg |
⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
| 5 |
3 4
|
syl |
⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
| 6 |
|
subgrcl |
⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
| 7 |
5 6
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
| 8 |
|
slwprm |
⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 ∈ ℙ ) |
| 9 |
3 8
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
| 10 |
1
|
grpbn0 |
⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ ) |
| 11 |
7 10
|
syl |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
| 12 |
|
hashnncl |
⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) ) |
| 13 |
2 12
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) ) |
| 14 |
11 13
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ ) |
| 15 |
9 14
|
pccld |
⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 ) |
| 16 |
|
pcdvds |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∥ ( ♯ ‘ 𝑋 ) ) |
| 17 |
9 14 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ∥ ( ♯ ‘ 𝑋 ) ) |
| 18 |
1 7 2 9 15 17
|
sylow1 |
⊢ ( 𝜑 → ∃ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 19 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑋 ∈ Fin ) |
| 20 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) |
| 21 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) |
| 22 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
| 23 |
|
eqid |
⊢ ( 𝐺 ↾s 𝐻 ) = ( 𝐺 ↾s 𝐻 ) |
| 24 |
23
|
slwpgp |
⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ) |
| 25 |
3 24
|
syl |
⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ) |
| 26 |
25
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) ) |
| 27 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 28 |
|
eqid |
⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 ) |
| 29 |
1 19 20 21 22 26 27 28
|
sylow2b |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 30 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 31 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ) |
| 32 |
31 8
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑃 ∈ ℙ ) |
| 33 |
15
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 ) |
| 34 |
21
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ) |
| 35 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑔 ∈ 𝑋 ) |
| 36 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) = ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) |
| 37 |
1 22 28 36
|
conjsubg |
⊢ ( ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝑋 ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
| 38 |
34 35 37
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) |
| 39 |
|
eqid |
⊢ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) = ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 40 |
39
|
subgbas |
⊢ ( ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) = ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) |
| 41 |
38 40
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) = ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) |
| 42 |
41
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) ) |
| 43 |
1 22 28 36
|
conjsubgen |
⊢ ( ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑔 ∈ 𝑋 ) → 𝑘 ≈ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 44 |
34 35 43
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑘 ≈ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 45 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑋 ∈ Fin ) |
| 46 |
1
|
subgss |
⊢ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) → 𝑘 ⊆ 𝑋 ) |
| 47 |
34 46
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑘 ⊆ 𝑋 ) |
| 48 |
45 47
|
ssfid |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑘 ∈ Fin ) |
| 49 |
1
|
subgss |
⊢ ( ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ⊆ 𝑋 ) |
| 50 |
38 49
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ⊆ 𝑋 ) |
| 51 |
45 50
|
ssfid |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ Fin ) |
| 52 |
|
hashen |
⊢ ( ( 𝑘 ∈ Fin ∧ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑘 ) = ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ↔ 𝑘 ≈ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 53 |
48 51 52
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ( ♯ ‘ 𝑘 ) = ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ↔ 𝑘 ≈ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 54 |
44 53
|
mpbird |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ 𝑘 ) = ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 55 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 56 |
54 55
|
eqtr3d |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 57 |
42 56
|
eqtr3d |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 58 |
|
oveq2 |
⊢ ( 𝑛 = ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 59 |
58
|
rspceeqv |
⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 ∧ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ 𝑛 ) ) |
| 60 |
33 57 59
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ 𝑛 ) ) |
| 61 |
39
|
subggrp |
⊢ ( ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ∈ Grp ) |
| 62 |
38 61
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ∈ Grp ) |
| 63 |
41 51
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ∈ Fin ) |
| 64 |
|
eqid |
⊢ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) = ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 65 |
64
|
pgpfi |
⊢ ( ( ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ∈ Fin ) → ( 𝑃 pGrp ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) ) |
| 66 |
62 63 65
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( 𝑃 pGrp ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ) = ( 𝑃 ↑ 𝑛 ) ) ) ) |
| 67 |
32 60 66
|
mpbir2and |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 68 |
39
|
slwispgp |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∧ 𝑃 pGrp ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ↔ 𝐻 = ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 69 |
31 38 68
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ( 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ∧ 𝑃 pGrp ( 𝐺 ↾s ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) ↔ 𝐻 = ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 70 |
30 67 69
|
mpbi2and |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → 𝐻 = ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) |
| 71 |
70
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) |
| 72 |
71 56
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ∧ 𝐻 ⊆ ran ( 𝑥 ∈ 𝑘 ↦ ( ( 𝑔 ( +g ‘ 𝐺 ) 𝑥 ) ( -g ‘ 𝐺 ) 𝑔 ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 73 |
29 72
|
rexlimddv |
⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑘 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |
| 74 |
18 73
|
rexlimddv |
⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) |