MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylow2blem3 Structured version   Visualization version   GIF version

Theorem sylow2blem3 17953
Description: Sylow's second theorem. Putting together the results of sylow2a 17950 and the orbit-stabilizer theorem to show that 𝑃 does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some 𝑔𝑋 with 𝑔𝐾 = 𝑔𝐾 for all 𝐻. This implies that invg(𝑔)𝑔𝐾, so is in the conjugated subgroup 𝑔𝐾invg(𝑔). (Contributed by Mario Carneiro, 18-Jan-2015.)
Hypotheses
Ref Expression
sylow2b.x 𝑋 = (Base‘𝐺)
sylow2b.xf (𝜑𝑋 ∈ Fin)
sylow2b.h (𝜑𝐻 ∈ (SubGrp‘𝐺))
sylow2b.k (𝜑𝐾 ∈ (SubGrp‘𝐺))
sylow2b.a + = (+g𝐺)
sylow2b.r = (𝐺 ~QG 𝐾)
sylow2b.m · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
sylow2blem3.hp (𝜑𝑃 pGrp (𝐺s 𝐻))
sylow2blem3.kn (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
sylow2blem3.d = (-g𝐺)
Assertion
Ref Expression
sylow2blem3 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Distinct variable groups:   𝑥,𝑔,𝑦,𝑧,𝐺   𝑔,𝐾,𝑥,𝑦,𝑧   · ,𝑔,𝑥,𝑦,𝑧   + ,𝑔,𝑥,𝑦,𝑧   ,𝑔,𝑥,𝑦,𝑧   𝜑,𝑔,𝑧   𝑥, ,𝑧   𝑔,𝐻,𝑥,𝑦,𝑧   𝑔,𝑋,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑃(𝑥,𝑦,𝑧,𝑔)   (𝑦,𝑔)

Proof of Theorem sylow2blem3
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 sylow2blem3.hp . . . . . . . . 9 (𝜑𝑃 pGrp (𝐺s 𝐻))
2 pgpprm 17924 . . . . . . . . 9 (𝑃 pGrp (𝐺s 𝐻) → 𝑃 ∈ ℙ)
31, 2syl 17 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
4 sylow2b.h . . . . . . . . . . 11 (𝜑𝐻 ∈ (SubGrp‘𝐺))
5 subgrcl 17515 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
7 sylow2b.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
87grpbn0 17367 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
96, 8syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
10 sylow2b.xf . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
11 hashnncl 13094 . . . . . . . . . 10 (𝑋 ∈ Fin → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1210, 11syl 17 . . . . . . . . 9 (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
139, 12mpbird 247 . . . . . . . 8 (𝜑 → (#‘𝑋) ∈ ℕ)
14 pcndvds2 15491 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (#‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
153, 13, 14syl2anc 692 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
16 sylow2b.r . . . . . . . . . . 11 = (𝐺 ~QG 𝐾)
17 sylow2b.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (SubGrp‘𝐺))
187, 16, 17, 10lagsubg2 17571 . . . . . . . . . 10 (𝜑 → (#‘𝑋) = ((#‘(𝑋 / )) · (#‘𝐾)))
1918oveq1d 6620 . . . . . . . . 9 (𝜑 → ((#‘𝑋) / (#‘𝐾)) = (((#‘(𝑋 / )) · (#‘𝐾)) / (#‘𝐾)))
20 sylow2blem3.kn . . . . . . . . . 10 (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
2120oveq2d 6621 . . . . . . . . 9 (𝜑 → ((#‘𝑋) / (#‘𝐾)) = ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
22 pwfi 8206 . . . . . . . . . . . . . 14 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
2310, 22sylib 208 . . . . . . . . . . . . 13 (𝜑 → 𝒫 𝑋 ∈ Fin)
247, 16eqger 17560 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → Er 𝑋)
2517, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 Er 𝑋)
2625qsss 7754 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / ) ⊆ 𝒫 𝑋)
27 ssfi 8125 . . . . . . . . . . . . 13 ((𝒫 𝑋 ∈ Fin ∧ (𝑋 / ) ⊆ 𝒫 𝑋) → (𝑋 / ) ∈ Fin)
2823, 26, 27syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝑋 / ) ∈ Fin)
29 hashcl 13084 . . . . . . . . . . . 12 ((𝑋 / ) ∈ Fin → (#‘(𝑋 / )) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . 11 (𝜑 → (#‘(𝑋 / )) ∈ ℕ0)
3130nn0cnd 11298 . . . . . . . . . 10 (𝜑 → (#‘(𝑋 / )) ∈ ℂ)
32 eqid 2626 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
3332subg0cl 17518 . . . . . . . . . . . . . 14 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3417, 33syl 17 . . . . . . . . . . . . 13 (𝜑 → (0g𝐺) ∈ 𝐾)
35 ne0i 3902 . . . . . . . . . . . . 13 ((0g𝐺) ∈ 𝐾𝐾 ≠ ∅)
3634, 35syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≠ ∅)
377subgss 17511 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3817, 37syl 17 . . . . . . . . . . . . . 14 (𝜑𝐾𝑋)
39 ssfi 8125 . . . . . . . . . . . . . 14 ((𝑋 ∈ Fin ∧ 𝐾𝑋) → 𝐾 ∈ Fin)
4010, 38, 39syl2anc 692 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
41 hashnncl 13094 . . . . . . . . . . . . 13 (𝐾 ∈ Fin → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4240, 41syl 17 . . . . . . . . . . . 12 (𝜑 → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4336, 42mpbird 247 . . . . . . . . . . 11 (𝜑 → (#‘𝐾) ∈ ℕ)
4443nncnd 10981 . . . . . . . . . 10 (𝜑 → (#‘𝐾) ∈ ℂ)
4543nnne0d 11010 . . . . . . . . . 10 (𝜑 → (#‘𝐾) ≠ 0)
4631, 44, 45divcan4d 10752 . . . . . . . . 9 (𝜑 → (((#‘(𝑋 / )) · (#‘𝐾)) / (#‘𝐾)) = (#‘(𝑋 / )))
4719, 21, 463eqtr3d 2668 . . . . . . . 8 (𝜑 → ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (#‘(𝑋 / )))
4847breq2d 4630 . . . . . . 7 (𝜑 → (𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) ↔ 𝑃 ∥ (#‘(𝑋 / ))))
4915, 48mtbid 314 . . . . . 6 (𝜑 → ¬ 𝑃 ∥ (#‘(𝑋 / )))
50 prmz 15308 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
513, 50syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
5230nn0zd 11424 . . . . . . 7 (𝜑 → (#‘(𝑋 / )) ∈ ℤ)
53 ssrab2 3671 . . . . . . . . . 10 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )
54 ssfi 8125 . . . . . . . . . 10 (((𝑋 / ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
5528, 53, 54sylancl 693 . . . . . . . . 9 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
56 hashcl 13084 . . . . . . . . 9 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5755, 56syl 17 . . . . . . . 8 (𝜑 → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5857nn0zd 11424 . . . . . . 7 (𝜑 → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
59 eqid 2626 . . . . . . . 8 (Base‘(𝐺s 𝐻)) = (Base‘(𝐺s 𝐻))
60 sylow2b.a . . . . . . . . 9 + = (+g𝐺)
61 sylow2b.m . . . . . . . . 9 · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
627, 10, 4, 17, 60, 16, 61sylow2blem2 17952 . . . . . . . 8 (𝜑· ∈ ((𝐺s 𝐻) GrpAct (𝑋 / )))
63 eqid 2626 . . . . . . . . . . 11 (𝐺s 𝐻) = (𝐺s 𝐻)
6463subgbas 17514 . . . . . . . . . 10 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺s 𝐻)))
654, 64syl 17 . . . . . . . . 9 (𝜑𝐻 = (Base‘(𝐺s 𝐻)))
667subgss 17511 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻𝑋)
674, 66syl 17 . . . . . . . . . 10 (𝜑𝐻𝑋)
68 ssfi 8125 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝐻𝑋) → 𝐻 ∈ Fin)
6910, 67, 68syl2anc 692 . . . . . . . . 9 (𝜑𝐻 ∈ Fin)
7065, 69eqeltrrd 2705 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝐻)) ∈ Fin)
71 eqid 2626 . . . . . . . 8 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}
72 eqid 2626 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)}
7359, 62, 1, 70, 28, 71, 72sylow2a 17950 . . . . . . 7 (𝜑𝑃 ∥ ((#‘(𝑋 / )) − (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
74 dvdssub2 14942 . . . . . . 7 (((𝑃 ∈ ℤ ∧ (#‘(𝑋 / )) ∈ ℤ ∧ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((#‘(𝑋 / )) − (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (#‘(𝑋 / )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7551, 52, 58, 73, 74syl31anc 1326 . . . . . 6 (𝜑 → (𝑃 ∥ (#‘(𝑋 / )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7649, 75mtbid 314 . . . . 5 (𝜑 → ¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))
77 hasheq0 13091 . . . . . . . 8 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
7855, 77syl 17 . . . . . . 7 (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
79 dvds0 14916 . . . . . . . . 9 (𝑃 ∈ ℤ → 𝑃 ∥ 0)
8051, 79syl 17 . . . . . . . 8 (𝜑𝑃 ∥ 0)
81 breq2 4622 . . . . . . . 8 ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0))
8280, 81syl5ibrcom 237 . . . . . . 7 (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
8378, 82sylbird 250 . . . . . 6 (𝜑 → ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
8483necon3bd 2810 . . . . 5 (𝜑 → (¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
8576, 84mpd 15 . . . 4 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
86 rabn0 3937 . . . 4 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8785, 86sylib 208 . . 3 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8865raleqdv 3138 . . . 4 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8988rexbidv 3050 . . 3 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
9087, 89mpbird 247 . 2 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧)
91 vex 3194 . . . . 5 𝑧 ∈ V
9291elqs 7745 . . . 4 (𝑧 ∈ (𝑋 / ) ↔ ∃𝑔𝑋 𝑧 = [𝑔] )
93 simplrr 800 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] )
9493oveq2d 6621 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ))
95 simprr 795 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
96 simpll 789 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
97 simprl 793 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝐻)
98 simplrl 799 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔𝑋)
997, 10, 4, 17, 60, 16, 61sylow2blem1 17951 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝐻𝑔𝑋) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
10096, 97, 98, 99syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
10194, 95, 1003eqtr3d 2668 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] )
10293, 101eqtr3d 2662 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] = [(𝑢 + 𝑔)] )
10325ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → Er 𝑋)
104103, 98erth 7737 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ [𝑔] = [(𝑢 + 𝑔)] ))
105102, 104mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 (𝑢 + 𝑔))
1066ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
10738ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾𝑋)
108 eqid 2626 . . . . . . . . . . . . . . . . . . . 20 (invg𝐺) = (invg𝐺)
1097, 108, 60, 16eqgval 17559 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐾𝑋) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
110106, 107, 109syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
111105, 110mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
112111simp3d 1073 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
113 oveq2 6613 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
114113oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) 𝑔) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
115 eqid 2626 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) = (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))
116 ovex 6633 . . . . . . . . . . . . . . . . 17 ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) ∈ V
117114, 115, 116fvmpt 6240 . . . . . . . . . . . . . . . 16 ((((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
118112, 117syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
1197, 60, 32, 108grprinv 17385 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
120106, 98, 119syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
121120oveq1d 6620 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g𝐺) + (𝑢 + 𝑔)))
1227, 108grpinvcl 17383 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → ((invg𝐺)‘𝑔) ∈ 𝑋)
123106, 98, 122syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg𝐺)‘𝑔) ∈ 𝑋)
12467ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻𝑋)
125124, 97sseldd 3589 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝑋)
1267, 60grpcl 17346 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
127106, 125, 98, 126syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
1287, 60grpass 17347 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑔𝑋 ∧ ((invg𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
129106, 98, 123, 127, 128syl13anc 1325 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
1307, 60, 32grplid 17368 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
131106, 127, 130syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
132121, 129, 1313eqtr3d 2668 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
133132oveq1d 6620 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) = ((𝑢 + 𝑔) 𝑔))
134 sylow2blem3.d . . . . . . . . . . . . . . . . 17 = (-g𝐺)
1357, 60, 134grppncan 17422 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
136106, 125, 98, 135syl3anc 1323 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
137118, 133, 1363eqtrd 2664 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
138 ovex 6633 . . . . . . . . . . . . . . . 16 ((𝑔 + 𝑥) 𝑔) ∈ V
139138, 115fnmpti 5981 . . . . . . . . . . . . . . 15 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾
140 fnfvelrn 6313 . . . . . . . . . . . . . . 15 (((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
141139, 112, 140sylancr 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
142137, 141eqeltrrd 2705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
143142expr 642 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ 𝑢𝐻) → ((𝑢 · 𝑧) = 𝑧𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
144143ralimdva 2961 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
145144imp 445 . . . . . . . . . 10 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
146145an32s 845 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
147 dfss3 3578 . . . . . . . . 9 (𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) ↔ ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
148146, 147sylibr 224 . . . . . . . 8 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
149148expr 642 . . . . . . 7 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔𝑋) → (𝑧 = [𝑔] 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
150149reximdva 3016 . . . . . 6 ((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
151150ex 450 . . . . 5 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
152151com23 86 . . . 4 (𝜑 → (∃𝑔𝑋 𝑧 = [𝑔] → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
15392, 152syl5bi 232 . . 3 (𝜑 → (𝑧 ∈ (𝑋 / ) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
154153rexlimdv 3028 . 2 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
15590, 154mpd 15 1 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1992  wne 2796  wral 2912  wrex 2913  {crab 2916  wss 3560  c0 3896  𝒫 cpw 4135  {cpr 4155   class class class wbr 4618  {copab 4677  cmpt 4678  ran crn 5080   Fn wfn 5845  cfv 5850  (class class class)co 6605  cmpt2 6607   Er wer 7685  [cec 7686   / cqs 7687  Fincfn 7900  0cc0 9881   · cmul 9886  cmin 10211   / cdiv 10629  cn 10965  0cn0 11237  cz 11322  cexp 12797  #chash 13054  cdvds 14902  cprime 15304   pCnt cpc 15460  Basecbs 15776  s cress 15777  +gcplusg 15857  0gc0g 16016  Grpcgrp 17338  invgcminusg 17339  -gcsg 17340  SubGrpcsubg 17504   ~QG cqg 17506   pGrp cpgp 17862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-omul 7511  df-er 7688  df-ec 7690  df-qs 7694  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-oi 8360  df-card 8710  df-acn 8713  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-n0 11238  df-xnn0 11309  df-z 11323  df-uz 11632  df-q 11733  df-rp 11777  df-fz 12266  df-fzo 12404  df-fl 12530  df-mod 12606  df-seq 12739  df-exp 12798  df-fac 12998  df-bc 13027  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-clim 14148  df-sum 14346  df-dvds 14903  df-gcd 15136  df-prm 15305  df-pc 15461  df-ndx 15779  df-slot 15780  df-base 15781  df-sets 15782  df-ress 15783  df-plusg 15870  df-0g 16018  df-mgm 17158  df-sgrp 17200  df-mnd 17211  df-submnd 17252  df-grp 17341  df-minusg 17342  df-sbg 17343  df-mulg 17457  df-subg 17507  df-eqg 17509  df-ga 17639  df-od 17864  df-pgp 17866
This theorem is referenced by:  sylow2b  17954
  Copyright terms: Public domain W3C validator