| Step | Hyp | Ref
| Expression |
| 1 | | sylow2blem3.hp |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
| 2 | | pgpprm 19611 |
. . . . . . . . 9
⊢ (𝑃 pGrp (𝐺 ↾s 𝐻) → 𝑃 ∈ ℙ) |
| 3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 4 | | sylow2b.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
| 5 | | subgrcl 19149 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 7 | | sylow2b.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
| 8 | 7 | grpbn0 18984 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
| 9 | 6, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 10 | | sylow2b.xf |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 11 | | hashnncl 14405 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
| 13 | 9, 12 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ) |
| 14 | | pcndvds2 16906 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝑋) ∈
ℕ) → ¬ 𝑃
∥ ((♯‘𝑋)
/ (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 15 | 3, 13, 14 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 16 | | sylow2b.r |
. . . . . . . . . . 11
⊢ ∼ =
(𝐺 ~QG
𝐾) |
| 17 | | sylow2b.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
| 18 | 7, 16, 17, 10 | lagsubg2 19212 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) ·
(♯‘𝐾))) |
| 19 | 18 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = (((♯‘(𝑋 / ∼ )) ·
(♯‘𝐾)) /
(♯‘𝐾))) |
| 20 | | sylow2blem3.kn |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) |
| 21 | 20 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋))))) |
| 22 | | pwfi 9357 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
| 23 | 10, 22 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
| 24 | 7, 16 | eqger 19196 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
| 25 | 17, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∼ Er 𝑋) |
| 26 | 25 | qsss 8818 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 / ∼ ) ⊆ 𝒫
𝑋) |
| 27 | 23, 26 | ssfid 9301 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 / ∼ ) ∈
Fin) |
| 28 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ ((𝑋 / ∼ ) ∈ Fin →
(♯‘(𝑋 /
∼
)) ∈ ℕ0) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝑋 / ∼ )) ∈
ℕ0) |
| 30 | 29 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(𝑋 / ∼ )) ∈
ℂ) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 32 | 31 | subg0cl 19152 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐾) |
| 33 | 17, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐾) |
| 34 | 33 | ne0d 4342 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≠ ∅) |
| 35 | 7 | subgss 19145 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
| 36 | 17, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
| 37 | 10, 36 | ssfid 9301 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Fin) |
| 38 | | hashnncl 14405 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Fin →
((♯‘𝐾) ∈
ℕ ↔ 𝐾 ≠
∅)) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅)) |
| 40 | 34, 39 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐾) ∈
ℕ) |
| 41 | 40 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐾) ∈
ℂ) |
| 42 | 40 | nnne0d 12316 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐾) ≠ 0) |
| 43 | 30, 41, 42 | divcan4d 12049 |
. . . . . . . . 9
⊢ (𝜑 → (((♯‘(𝑋 / ∼ )) ·
(♯‘𝐾)) /
(♯‘𝐾)) =
(♯‘(𝑋 /
∼
))) |
| 44 | 19, 21, 43 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (♯‘(𝑋 / ∼
))) |
| 45 | 44 | breq2d 5155 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ↔ 𝑃 ∥ (♯‘(𝑋 / ∼
)))) |
| 46 | 15, 45 | mtbid 324 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝑋 / ∼
))) |
| 47 | | prmz 16712 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 48 | 3, 47 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 49 | 29 | nn0zd 12639 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑋 / ∼ )) ∈
ℤ) |
| 50 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ ) |
| 51 | | ssfi 9213 |
. . . . . . . . . 10
⊢ (((𝑋 / ∼ ) ∈ Fin ∧
{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ )) → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin) |
| 52 | 27, 50, 51 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin) |
| 53 | | hashcl 14395 |
. . . . . . . . 9
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈
ℕ0) |
| 54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈
ℕ0) |
| 55 | 54 | nn0zd 12639 |
. . . . . . 7
⊢ (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) |
| 56 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝐺
↾s 𝐻)) =
(Base‘(𝐺
↾s 𝐻)) |
| 57 | | sylow2b.a |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
| 58 | | sylow2b.m |
. . . . . . . . 9
⊢ · =
(𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 59 | 7, 10, 4, 17, 57, 16, 58 | sylow2blem2 19639 |
. . . . . . . 8
⊢ (𝜑 → · ∈ ((𝐺 ↾s 𝐻) GrpAct (𝑋 / ∼
))) |
| 60 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻) |
| 61 | 60 | subgbas 19148 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
| 62 | 4, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
| 63 | 7 | subgss 19145 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
| 64 | 4, 63 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ⊆ 𝑋) |
| 65 | 10, 64 | ssfid 9301 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ Fin) |
| 66 | 62, 65 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝐻)) ∈ Fin) |
| 67 | | eqid 2737 |
. . . . . . . 8
⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} |
| 68 | | eqid 2737 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧
∃𝑔 ∈
(Base‘(𝐺
↾s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧
∃𝑔 ∈
(Base‘(𝐺
↾s 𝐻))(𝑔 · 𝑥) = 𝑦)} |
| 69 | 56, 59, 1, 66, 27, 67, 68 | sylow2a 19637 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∥ ((♯‘(𝑋 / ∼ )) −
(♯‘{𝑧 ∈
(𝑋 / ∼ )
∣ ∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
| 70 | | dvdssub2 16338 |
. . . . . . 7
⊢ (((𝑃 ∈ ℤ ∧
(♯‘(𝑋 /
∼
)) ∈ ℤ ∧ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((♯‘(𝑋 / ∼ )) −
(♯‘{𝑧 ∈
(𝑋 / ∼ )
∣ ∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (♯‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
| 71 | 48, 49, 55, 69, 70 | syl31anc 1375 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ (♯‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
| 72 | 46, 71 | mtbid 324 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧})) |
| 73 | | hasheq0 14402 |
. . . . . . . 8
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅)) |
| 74 | 52, 73 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅)) |
| 75 | | dvds0 16309 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0) |
| 76 | 48, 75 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∥ 0) |
| 77 | | breq2 5147 |
. . . . . . . 8
⊢
((♯‘{𝑧
∈ (𝑋 / ∼ )
∣ ∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0)) |
| 78 | 76, 77 | syl5ibrcom 247 |
. . . . . . 7
⊢ (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
| 79 | 74, 78 | sylbird 260 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
| 80 | 79 | necon3bd 2954 |
. . . . 5
⊢ (𝜑 → (¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)) |
| 81 | 72, 80 | mpd 15 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅) |
| 82 | | rabn0 4389 |
. . . 4
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧) |
| 83 | 81, 82 | sylib 218 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧) |
| 84 | 62 | raleqdv 3326 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)) |
| 85 | 84 | rexbidv 3179 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)) |
| 86 | 83, 85 | mpbird 257 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) |
| 87 | | vex 3484 |
. . . . 5
⊢ 𝑧 ∈ V |
| 88 | 87 | elqs 8809 |
. . . 4
⊢ (𝑧 ∈ (𝑋 / ∼ ) ↔
∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ ) |
| 89 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] ∼ ) |
| 90 | 89 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ∼ )) |
| 91 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧) |
| 92 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑) |
| 93 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝐻) |
| 94 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∈ 𝑋) |
| 95 | 7, 10, 4, 17, 57, 16, 58 | sylow2blem1 19638 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑔 ∈ 𝑋) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ ) |
| 96 | 92, 93, 94, 95 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ ) |
| 97 | 90, 91, 96 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] ∼ ) |
| 98 | 89, 97 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ ) |
| 99 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ∼ Er 𝑋) |
| 100 | 99, 94 | erth 8796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ )) |
| 101 | 98, 100 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∼ (𝑢 + 𝑔)) |
| 102 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp) |
| 103 | 36 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾 ⊆ 𝑋) |
| 104 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 105 | 7, 104, 57, 16 | eqgval 19195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))) |
| 106 | 102, 103,
105 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))) |
| 107 | 101, 106 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)) |
| 108 | 107 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) |
| 109 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
| 110 | 109 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) − 𝑔) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
| 111 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) = (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) |
| 112 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) ∈ V |
| 113 | 110, 111,
112 | fvmpt 7016 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
| 114 | 108, 113 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
| 115 | 7, 57, 31, 104 | grprinv 19008 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → (𝑔 +
((invg‘𝐺)‘𝑔)) = (0g‘𝐺)) |
| 116 | 102, 94, 115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 +
((invg‘𝐺)‘𝑔)) = (0g‘𝐺)) |
| 117 | 116 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g‘𝐺) + (𝑢 + 𝑔))) |
| 118 | 7, 104 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → ((invg‘𝐺)‘𝑔) ∈ 𝑋) |
| 119 | 102, 94, 118 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg‘𝐺)‘𝑔) ∈ 𝑋) |
| 120 | 64 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻 ⊆ 𝑋) |
| 121 | 120, 93 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝑋) |
| 122 | 7, 57 | grpcl 18959 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑢 + 𝑔) ∈ 𝑋) |
| 123 | 102, 121,
94, 122 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋) |
| 124 | 7, 57 | grpass 18960 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ (𝑔 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
| 125 | 102, 94, 119, 123, 124 | syl13anc 1374 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
| 126 | 7, 57, 31 | grplid 18985 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔)) |
| 127 | 102, 123,
126 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔)) |
| 128 | 117, 125,
127 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔)) |
| 129 | 128 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) = ((𝑢 + 𝑔) − 𝑔)) |
| 130 | | sylow2blem3.d |
. . . . . . . . . . . . . . . . 17
⊢ − =
(-g‘𝐺) |
| 131 | 7, 57, 130 | grppncan 19049 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((𝑢 + 𝑔) − 𝑔) = 𝑢) |
| 132 | 102, 121,
94, 131 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) − 𝑔) = 𝑢) |
| 133 | 114, 129,
132 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢) |
| 134 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 + 𝑥) − 𝑔) ∈ V |
| 135 | 134, 111 | fnmpti 6711 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾 |
| 136 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 137 | 135, 108,
136 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 138 | 133, 137 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 139 | 138 | expr 456 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ 𝑢 ∈ 𝐻) → ((𝑢 · 𝑧) = 𝑧 → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
| 140 | 139 | ralimdva 3167 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
| 141 | 140 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧
∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 142 | 141 | an32s 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) →
∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 143 | | dfss3 3972 |
. . . . . . . . 9
⊢ (𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) ↔ ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 144 | 142, 143 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
| 145 | 144 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔 ∈ 𝑋) → (𝑧 = [𝑔] ∼ → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
| 146 | 145 | reximdva 3168 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
| 147 | 146 | ex 412 |
. . . . 5
⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
| 148 | 147 | com23 86 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
| 149 | 88, 148 | biimtrid 242 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑋 / ∼ ) →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
| 150 | 149 | rexlimdv 3153 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
| 151 | 86, 150 | mpd 15 |
1
⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |