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

Theorem sylow2blem3 18083
Description: Sylow's second theorem. Putting together the results of sylow2a 18080 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 18054 . . . . . . . . 9 (𝑃 pGrp (𝐺s 𝐻) → 𝑃 ∈ ℙ)
31, 2syl 17 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
4 sylow2b.h . . . . . . . . . . 11 (𝜑𝐻 ∈ (SubGrp‘𝐺))
5 subgrcl 17646 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
7 sylow2b.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
87grpbn0 17498 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
96, 8syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
10 sylow2b.xf . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
11 hashnncl 13195 . . . . . . . . . 10 (𝑋 ∈ Fin → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1210, 11syl 17 . . . . . . . . 9 (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
139, 12mpbird 247 . . . . . . . 8 (𝜑 → (#‘𝑋) ∈ ℕ)
14 pcndvds2 15619 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (#‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
153, 13, 14syl2anc 694 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
16 sylow2b.r . . . . . . . . . . 11 = (𝐺 ~QG 𝐾)
17 sylow2b.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (SubGrp‘𝐺))
187, 16, 17, 10lagsubg2 17702 . . . . . . . . . 10 (𝜑 → (#‘𝑋) = ((#‘(𝑋 / )) · (#‘𝐾)))
1918oveq1d 6705 . . . . . . . . 9 (𝜑 → ((#‘𝑋) / (#‘𝐾)) = (((#‘(𝑋 / )) · (#‘𝐾)) / (#‘𝐾)))
20 sylow2blem3.kn . . . . . . . . . 10 (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
2120oveq2d 6706 . . . . . . . . 9 (𝜑 → ((#‘𝑋) / (#‘𝐾)) = ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))))
22 pwfi 8302 . . . . . . . . . . . . . 14 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
2310, 22sylib 208 . . . . . . . . . . . . 13 (𝜑 → 𝒫 𝑋 ∈ Fin)
247, 16eqger 17691 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → Er 𝑋)
2517, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 Er 𝑋)
2625qsss 7851 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / ) ⊆ 𝒫 𝑋)
27 ssfi 8221 . . . . . . . . . . . . 13 ((𝒫 𝑋 ∈ Fin ∧ (𝑋 / ) ⊆ 𝒫 𝑋) → (𝑋 / ) ∈ Fin)
2823, 26, 27syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝑋 / ) ∈ Fin)
29 hashcl 13185 . . . . . . . . . . . 12 ((𝑋 / ) ∈ Fin → (#‘(𝑋 / )) ∈ ℕ0)
3028, 29syl 17 . . . . . . . . . . 11 (𝜑 → (#‘(𝑋 / )) ∈ ℕ0)
3130nn0cnd 11391 . . . . . . . . . 10 (𝜑 → (#‘(𝑋 / )) ∈ ℂ)
32 eqid 2651 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
3332subg0cl 17649 . . . . . . . . . . . . . 14 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3417, 33syl 17 . . . . . . . . . . . . 13 (𝜑 → (0g𝐺) ∈ 𝐾)
35 ne0i 3954 . . . . . . . . . . . . 13 ((0g𝐺) ∈ 𝐾𝐾 ≠ ∅)
3634, 35syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≠ ∅)
377subgss 17642 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3817, 37syl 17 . . . . . . . . . . . . . 14 (𝜑𝐾𝑋)
39 ssfi 8221 . . . . . . . . . . . . . 14 ((𝑋 ∈ Fin ∧ 𝐾𝑋) → 𝐾 ∈ Fin)
4010, 38, 39syl2anc 694 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
41 hashnncl 13195 . . . . . . . . . . . . 13 (𝐾 ∈ Fin → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4240, 41syl 17 . . . . . . . . . . . 12 (𝜑 → ((#‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4336, 42mpbird 247 . . . . . . . . . . 11 (𝜑 → (#‘𝐾) ∈ ℕ)
4443nncnd 11074 . . . . . . . . . 10 (𝜑 → (#‘𝐾) ∈ ℂ)
4543nnne0d 11103 . . . . . . . . . 10 (𝜑 → (#‘𝐾) ≠ 0)
4631, 44, 45divcan4d 10845 . . . . . . . . 9 (𝜑 → (((#‘(𝑋 / )) · (#‘𝐾)) / (#‘𝐾)) = (#‘(𝑋 / )))
4719, 21, 463eqtr3d 2693 . . . . . . . 8 (𝜑 → ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) = (#‘(𝑋 / )))
4847breq2d 4697 . . . . . . 7 (𝜑 → (𝑃 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) ↔ 𝑃 ∥ (#‘(𝑋 / ))))
4915, 48mtbid 313 . . . . . 6 (𝜑 → ¬ 𝑃 ∥ (#‘(𝑋 / )))
50 prmz 15436 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
513, 50syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
5230nn0zd 11518 . . . . . . 7 (𝜑 → (#‘(𝑋 / )) ∈ ℤ)
53 ssrab2 3720 . . . . . . . . . 10 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )
54 ssfi 8221 . . . . . . . . . 10 (((𝑋 / ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
5528, 53, 54sylancl 695 . . . . . . . . 9 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
56 hashcl 13185 . . . . . . . . 9 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5755, 56syl 17 . . . . . . . 8 (𝜑 → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5857nn0zd 11518 . . . . . . 7 (𝜑 → (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
59 eqid 2651 . . . . . . . 8 (Base‘(𝐺s 𝐻)) = (Base‘(𝐺s 𝐻))
60 sylow2b.a . . . . . . . . 9 + = (+g𝐺)
61 sylow2b.m . . . . . . . . 9 · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
627, 10, 4, 17, 60, 16, 61sylow2blem2 18082 . . . . . . . 8 (𝜑· ∈ ((𝐺s 𝐻) GrpAct (𝑋 / )))
63 eqid 2651 . . . . . . . . . . 11 (𝐺s 𝐻) = (𝐺s 𝐻)
6463subgbas 17645 . . . . . . . . . 10 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺s 𝐻)))
654, 64syl 17 . . . . . . . . 9 (𝜑𝐻 = (Base‘(𝐺s 𝐻)))
667subgss 17642 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻𝑋)
674, 66syl 17 . . . . . . . . . 10 (𝜑𝐻𝑋)
68 ssfi 8221 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝐻𝑋) → 𝐻 ∈ Fin)
6910, 67, 68syl2anc 694 . . . . . . . . 9 (𝜑𝐻 ∈ Fin)
7065, 69eqeltrrd 2731 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝐻)) ∈ Fin)
71 eqid 2651 . . . . . . . 8 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}
72 eqid 2651 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)}
7359, 62, 1, 70, 28, 71, 72sylow2a 18080 . . . . . . 7 (𝜑𝑃 ∥ ((#‘(𝑋 / )) − (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
74 dvdssub2 15070 . . . . . . 7 (((𝑃 ∈ ℤ ∧ (#‘(𝑋 / )) ∈ ℤ ∧ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((#‘(𝑋 / )) − (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (#‘(𝑋 / )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7551, 52, 58, 73, 74syl31anc 1369 . . . . . 6 (𝜑 → (𝑃 ∥ (#‘(𝑋 / )) ↔ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7649, 75mtbid 313 . . . . 5 (𝜑 → ¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))
77 hasheq0 13192 . . . . . . . 8 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
7855, 77syl 17 . . . . . . 7 (𝜑 → ((#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
79 dvds0 15044 . . . . . . . . 9 (𝑃 ∈ ℤ → 𝑃 ∥ 0)
8051, 79syl 17 . . . . . . . 8 (𝜑𝑃 ∥ 0)
81 breq2 4689 . . . . . . . 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 2837 . . . . 5 (𝜑 → (¬ 𝑃 ∥ (#‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
8576, 84mpd 15 . . . 4 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
86 rabn0 3991 . . . 4 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8785, 86sylib 208 . . 3 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8865raleqdv 3174 . . . 4 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8988rexbidv 3081 . . 3 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
9087, 89mpbird 247 . 2 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧)
91 vex 3234 . . . . 5 𝑧 ∈ V
9291elqs 7842 . . . 4 (𝑧 ∈ (𝑋 / ) ↔ ∃𝑔𝑋 𝑧 = [𝑔] )
93 simplrr 818 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] )
9493oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ))
95 simprr 811 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
96 simpll 805 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
97 simprl 809 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝐻)
98 simplrl 817 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔𝑋)
997, 10, 4, 17, 60, 16, 61sylow2blem1 18081 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝐻𝑔𝑋) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
10096, 97, 98, 99syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
10194, 95, 1003eqtr3d 2693 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] )
10293, 101eqtr3d 2687 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] = [(𝑢 + 𝑔)] )
10325ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → Er 𝑋)
104103, 98erth 7834 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ [𝑔] = [(𝑢 + 𝑔)] ))
105102, 104mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 (𝑢 + 𝑔))
1066ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
10738ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾𝑋)
108 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (invg𝐺) = (invg𝐺)
1097, 108, 60, 16eqgval 17690 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐾𝑋) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
110106, 107, 109syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
111105, 110mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
112111simp3d 1095 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
113 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
114113oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) 𝑔) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
115 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) = (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))
116 ovex 6718 . . . . . . . . . . . . . . . . 17 ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) ∈ V
117114, 115, 116fvmpt 6321 . . . . . . . . . . . . . . . 16 ((((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
118112, 117syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
1197, 60, 32, 108grprinv 17516 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
120106, 98, 119syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
121120oveq1d 6705 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g𝐺) + (𝑢 + 𝑔)))
1227, 108grpinvcl 17514 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → ((invg𝐺)‘𝑔) ∈ 𝑋)
123106, 98, 122syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg𝐺)‘𝑔) ∈ 𝑋)
12467ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻𝑋)
125124, 97sseldd 3637 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝑋)
1267, 60grpcl 17477 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
127106, 125, 98, 126syl3anc 1366 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
1287, 60grpass 17478 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑔𝑋 ∧ ((invg𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
129106, 98, 123, 127, 128syl13anc 1368 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
1307, 60, 32grplid 17499 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
131106, 127, 130syl2anc 694 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
132121, 129, 1313eqtr3d 2693 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
133132oveq1d 6705 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) = ((𝑢 + 𝑔) 𝑔))
134 sylow2blem3.d . . . . . . . . . . . . . . . . 17 = (-g𝐺)
1357, 60, 134grppncan 17553 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
136106, 125, 98, 135syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
137118, 133, 1363eqtrd 2689 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
138 ovex 6718 . . . . . . . . . . . . . . . 16 ((𝑔 + 𝑥) 𝑔) ∈ V
139138, 115fnmpti 6060 . . . . . . . . . . . . . . 15 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾
140 fnfvelrn 6396 . . . . . . . . . . . . . . 15 (((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
141139, 112, 140sylancr 696 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
142137, 141eqeltrrd 2731 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
143142expr 642 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ 𝑢𝐻) → ((𝑢 · 𝑧) = 𝑧𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
144143ralimdva 2991 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
145144imp 444 . . . . . . . . . 10 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
146145an32s 863 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
147 dfss3 3625 . . . . . . . . 9 (𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) ↔ ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
148146, 147sylibr 224 . . . . . . . 8 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
149148expr 642 . . . . . . 7 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔𝑋) → (𝑧 = [𝑔] 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
150149reximdva 3046 . . . . . 6 ((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
151150ex 449 . . . . 5 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
152151com23 86 . . . 4 (𝜑 → (∃𝑔𝑋 𝑧 = [𝑔] → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
15392, 152syl5bi 232 . . 3 (𝜑 → (𝑧 ∈ (𝑋 / ) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
154153rexlimdv 3059 . 2 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
15590, 154mpd 15 1 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  wss 3607  c0 3948  𝒫 cpw 4191  {cpr 4212   class class class wbr 4685  {copab 4745  cmpt 4762  ran crn 5144   Fn wfn 5921  cfv 5926  (class class class)co 6690  cmpt2 6692   Er wer 7784  [cec 7785   / cqs 7786  Fincfn 7997  0cc0 9974   · cmul 9979  cmin 10304   / cdiv 10722  cn 11058  0cn0 11330  cz 11415  cexp 12900  #chash 13157  cdvds 15027  cprime 15432   pCnt cpc 15588  Basecbs 15904  s cress 15905  +gcplusg 15988  0gc0g 16147  Grpcgrp 17469  invgcminusg 17470  -gcsg 17471  SubGrpcsubg 17635   ~QG cqg 17637   pGrp cpgp 17992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-er 7787  df-ec 7789  df-qs 7793  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-grp 17472  df-minusg 17473  df-sbg 17474  df-mulg 17588  df-subg 17638  df-eqg 17640  df-ga 17769  df-od 17994  df-pgp 17996
This theorem is referenced by:  sylow2b  18084
  Copyright terms: Public domain W3C validator