Step | Hyp | Ref
| Expression |
1 | | sylow2blem3.hp |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻)) |
2 | | pgpprm 18008 |
. . . . . . . . 9
⊢ (𝑃 pGrp (𝐺 ↾s 𝐻) → 𝑃 ∈ ℙ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℙ) |
4 | | sylow2b.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
5 | | subgrcl 17599 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ Grp) |
7 | | sylow2b.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
8 | 7 | grpbn0 17451 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
9 | 6, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≠ ∅) |
10 | | sylow2b.xf |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ Fin) |
11 | | hashnncl 13157 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
13 | 9, 12 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
14 | | pcndvds2 15572 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝑋) ∈ ℕ)
→ ¬ 𝑃 ∥
((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
15 | 3, 13, 14 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
16 | | sylow2b.r |
. . . . . . . . . . 11
⊢ ∼ =
(𝐺 ~QG
𝐾) |
17 | | sylow2b.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
18 | 7, 16, 17, 10 | lagsubg2 17655 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑋) = ((#‘(𝑋 / ∼ )) ·
(#‘𝐾))) |
19 | 18 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑋) / (#‘𝐾)) = (((#‘(𝑋 / ∼ )) ·
(#‘𝐾)) /
(#‘𝐾))) |
20 | | sylow2blem3.kn |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) |
21 | 20 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝑋) / (#‘𝐾)) = ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋))))) |
22 | | pwfi 8261 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
23 | 10, 22 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
24 | 7, 16 | eqger 17644 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∼ Er 𝑋) |
26 | 25 | qsss 7808 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 / ∼ ) ⊆ 𝒫
𝑋) |
27 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢
((𝒫 𝑋 ∈
Fin ∧ (𝑋 / ∼ )
⊆ 𝒫 𝑋) →
(𝑋 / ∼ )
∈ Fin) |
28 | 23, 26, 27 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 / ∼ ) ∈
Fin) |
29 | | hashcl 13147 |
. . . . . . . . . . . 12
⊢ ((𝑋 / ∼ ) ∈ Fin →
(#‘(𝑋 / ∼ ))
∈ ℕ0) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈
ℕ0) |
31 | 30 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈
ℂ) |
32 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
33 | 32 | subg0cl 17602 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐾) |
34 | 17, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐾) |
35 | | ne0i 3921 |
. . . . . . . . . . . . 13
⊢
((0g‘𝐺) ∈ 𝐾 → 𝐾 ≠ ∅) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ≠ ∅) |
37 | 7 | subgss 17595 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
38 | 17, 37 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
39 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ Fin ∧ 𝐾 ⊆ 𝑋) → 𝐾 ∈ Fin) |
40 | 10, 38, 39 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Fin) |
41 | | hashnncl 13157 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ Fin →
((#‘𝐾) ∈ ℕ
↔ 𝐾 ≠
∅)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅)) |
43 | 36, 42 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐾) ∈ ℕ) |
44 | 43 | nncnd 11036 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐾) ∈ ℂ) |
45 | 43 | nnne0d 11065 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐾) ≠ 0) |
46 | 31, 44, 45 | divcan4d 10807 |
. . . . . . . . 9
⊢ (𝜑 → (((#‘(𝑋 / ∼ )) ·
(#‘𝐾)) /
(#‘𝐾)) =
(#‘(𝑋 / ∼
))) |
47 | 19, 21, 46 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (#‘(𝑋 / ∼
))) |
48 | 47 | breq2d 4665 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) ↔ 𝑃 ∥ (#‘(𝑋 / ∼
)))) |
49 | 15, 48 | mtbid 314 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 ∥ (#‘(𝑋 / ∼
))) |
50 | | prmz 15389 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
51 | 3, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℤ) |
52 | 30 | nn0zd 11480 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑋 / ∼ )) ∈
ℤ) |
53 | | ssrab2 3687 |
. . . . . . . . . 10
⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ ) |
54 | | ssfi 8180 |
. . . . . . . . . 10
⊢ (((𝑋 / ∼ ) ∈ Fin ∧
{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / ∼ )) → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin) |
55 | 28, 53, 54 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin) |
56 | | hashcl 13147 |
. . . . . . . . 9
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈
ℕ0) |
58 | 57 | nn0zd 11480 |
. . . . . . 7
⊢ (𝜑 → (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) |
59 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘(𝐺
↾s 𝐻)) =
(Base‘(𝐺
↾s 𝐻)) |
60 | | sylow2b.a |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
61 | | sylow2b.m |
. . . . . . . . 9
⊢ · =
(𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
62 | 7, 10, 4, 17, 60, 16, 61 | sylow2blem2 18036 |
. . . . . . . 8
⊢ (𝜑 → · ∈ ((𝐺 ↾s 𝐻) GrpAct (𝑋 / ∼
))) |
63 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝐺 ↾s 𝐻) = (𝐺 ↾s 𝐻) |
64 | 63 | subgbas 17598 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
65 | 4, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 = (Base‘(𝐺 ↾s 𝐻))) |
66 | 7 | subgss 17595 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
67 | 4, 66 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻 ⊆ 𝑋) |
68 | | ssfi 8180 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
69 | 10, 67, 68 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ Fin) |
70 | 65, 69 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → (Base‘(𝐺 ↾s 𝐻)) ∈ Fin) |
71 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} |
72 | | eqid 2622 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧
∃𝑔 ∈
(Base‘(𝐺
↾s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ∼ ) ∧
∃𝑔 ∈
(Base‘(𝐺
↾s 𝐻))(𝑔 · 𝑥) = 𝑦)} |
73 | 59, 62, 1, 70, 28, 71, 72 | sylow2a 18034 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∥ ((#‘(𝑋 / ∼ )) −
(#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
74 | | dvdssub2 15023 |
. . . . . . 7
⊢ (((𝑃 ∈ ℤ ∧
(#‘(𝑋 / ∼ ))
∈ ℤ ∧ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((#‘(𝑋 / ∼ )) −
(#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (#‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
75 | 51, 52, 58, 73, 74 | syl31anc 1329 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ (#‘(𝑋 / ∼ )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
76 | 49, 75 | mtbid 314 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧})) |
77 | | hasheq0 13154 |
. . . . . . . 8
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅)) |
78 | 55, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅)) |
79 | | dvds0 14997 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0) |
80 | 51, 79 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∥ 0) |
81 | | breq2 4657 |
. . . . . . . 8
⊢
((#‘{𝑧 ∈
(𝑋 / ∼ )
∣ ∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0)) |
82 | 80, 81 | syl5ibrcom 237 |
. . . . . . 7
⊢ (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
83 | 78, 82 | sylbird 250 |
. . . . . 6
⊢ (𝜑 → ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}))) |
84 | 83 | necon3bd 2808 |
. . . . 5
⊢ (𝜑 → (¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)) |
85 | 76, 84 | mpd 15 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅) |
86 | | rabn0 3958 |
. . . 4
⊢ ({𝑧 ∈ (𝑋 / ∼ ) ∣
∀𝑢 ∈
(Base‘(𝐺
↾s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧) |
87 | 85, 86 | sylib 208 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧) |
88 | 65 | raleqdv 3144 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)) |
89 | 88 | rexbidv 3052 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ (Base‘(𝐺 ↾s 𝐻))(𝑢 · 𝑧) = 𝑧)) |
90 | 87, 89 | mpbird 247 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) |
91 | | vex 3203 |
. . . . 5
⊢ 𝑧 ∈ V |
92 | 91 | elqs 7799 |
. . . 4
⊢ (𝑧 ∈ (𝑋 / ∼ ) ↔
∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ ) |
93 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] ∼ ) |
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ∼ )) |
95 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧) |
96 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑) |
97 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝐻) |
98 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∈ 𝑋) |
99 | 7, 10, 4, 17, 60, 16, 61 | sylow2blem1 18035 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐻 ∧ 𝑔 ∈ 𝑋) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ ) |
100 | 96, 97, 98, 99 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ∼ ) = [(𝑢 + 𝑔)] ∼ ) |
101 | 94, 95, 100 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] ∼ ) |
102 | 93, 101 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ ) |
103 | 25 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ∼ Er 𝑋) |
104 | 103, 98 | erth 7791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ [𝑔] ∼ = [(𝑢 + 𝑔)] ∼ )) |
105 | 102, 104 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 ∼ (𝑢 + 𝑔)) |
106 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp) |
107 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾 ⊆ 𝑋) |
108 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(invg‘𝐺) = (invg‘𝐺) |
109 | 7, 108, 60, 16 | eqgval 17643 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))) |
110 | 106, 107,
109 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∼ (𝑢 + 𝑔) ↔ (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))) |
111 | 105, 110 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)) |
112 | 111 | simp3d 1075 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) |
113 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
114 | 113 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) − 𝑔) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
115 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) = (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) |
116 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) ∈ V |
117 | 114, 115,
116 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
118 | 112, 117 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔)) |
119 | 7, 60, 32, 108 | grprinv 17469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → (𝑔 +
((invg‘𝐺)‘𝑔)) = (0g‘𝐺)) |
120 | 106, 98, 119 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 +
((invg‘𝐺)‘𝑔)) = (0g‘𝐺)) |
121 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g‘𝐺) + (𝑢 + 𝑔))) |
122 | 7, 108 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝑋) → ((invg‘𝐺)‘𝑔) ∈ 𝑋) |
123 | 106, 98, 122 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg‘𝐺)‘𝑔) ∈ 𝑋) |
124 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻 ⊆ 𝑋) |
125 | 124, 97 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ 𝑋) |
126 | 7, 60 | grpcl 17430 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑢 + 𝑔) ∈ 𝑋) |
127 | 106, 125,
98, 126 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋) |
128 | 7, 60 | grpass 17431 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ (𝑔 ∈ 𝑋 ∧ ((invg‘𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
129 | 106, 98, 123, 127, 128 | syl13anc 1328 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
((invg‘𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)))) |
130 | 7, 60, 32 | grplid 17452 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔)) |
131 | 106, 127,
130 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g‘𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔)) |
132 | 121, 129,
131 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔)) |
133 | 132 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 +
(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) − 𝑔) = ((𝑢 + 𝑔) − 𝑔)) |
134 | | sylow2blem3.d |
. . . . . . . . . . . . . . . . 17
⊢ − =
(-g‘𝐺) |
135 | 7, 60, 134 | grppncan 17506 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((𝑢 + 𝑔) − 𝑔) = 𝑢) |
136 | 106, 125,
98, 135 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) − 𝑔) = 𝑢) |
137 | 118, 133,
136 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢) |
138 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 + 𝑥) − 𝑔) ∈ V |
139 | 138, 115 | fnmpti 6022 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾 |
140 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) Fn 𝐾 ∧ (((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
141 | 139, 112,
140 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))‘(((invg‘𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
142 | 137, 141 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ (𝑢 ∈ 𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
143 | 142 | expr 643 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧ 𝑢 ∈ 𝐻) → ((𝑢 · 𝑧) = 𝑧 → 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
144 | 143 | ralimdva 2962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
145 | 144 | imp 445 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) ∧
∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
146 | 145 | an32s 846 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) →
∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
147 | | dfss3 3592 |
. . . . . . . . 9
⊢ (𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)) ↔ ∀𝑢 ∈ 𝐻 𝑢 ∈ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
148 | 146, 147 | sylibr 224 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔 ∈ 𝑋 ∧ 𝑧 = [𝑔] ∼ )) → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |
149 | 148 | expr 643 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔 ∈ 𝑋) → (𝑧 = [𝑔] ∼ → 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
150 | 149 | reximdva 3017 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
151 | 150 | ex 450 |
. . . . 5
⊢ (𝜑 → (∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
152 | 151 | com23 86 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ 𝑋 𝑧 = [𝑔] ∼ →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
153 | 92, 152 | syl5bi 232 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝑋 / ∼ ) →
(∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))))) |
154 | 153 | rexlimdv 3030 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ (𝑋 / ∼ )∀𝑢 ∈ 𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔)))) |
155 | 90, 154 | mpd 15 |
1
⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) |