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

Theorem sylow2blem3 19640
Description: Sylow's second theorem. Putting together the results of sylow2a 19637 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 19611 . . . . . . . . 9 (𝑃 pGrp (𝐺s 𝐻) → 𝑃 ∈ ℙ)
31, 2syl 17 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
4 sylow2b.h . . . . . . . . . . 11 (𝜑𝐻 ∈ (SubGrp‘𝐺))
5 subgrcl 19149 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
7 sylow2b.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
87grpbn0 18984 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
96, 8syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
10 sylow2b.xf . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
11 hashnncl 14405 . . . . . . . . . 10 (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1210, 11syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
139, 12mpbird 257 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ)
14 pcndvds2 16906 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (♯‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
153, 13, 14syl2anc 584 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
16 sylow2b.r . . . . . . . . . . 11 = (𝐺 ~QG 𝐾)
17 sylow2b.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (SubGrp‘𝐺))
187, 16, 17, 10lagsubg2 19212 . . . . . . . . . 10 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / )) · (♯‘𝐾)))
1918oveq1d 7446 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)))
20 sylow2blem3.kn . . . . . . . . . 10 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
2120oveq2d 7447 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
22 pwfi 9357 . . . . . . . . . . . . . 14 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
2310, 22sylib 218 . . . . . . . . . . . . 13 (𝜑 → 𝒫 𝑋 ∈ Fin)
247, 16eqger 19196 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → Er 𝑋)
2517, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 Er 𝑋)
2625qsss 8818 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / ) ⊆ 𝒫 𝑋)
2723, 26ssfid 9301 . . . . . . . . . . . 12 (𝜑 → (𝑋 / ) ∈ Fin)
28 hashcl 14395 . . . . . . . . . . . 12 ((𝑋 / ) ∈ Fin → (♯‘(𝑋 / )) ∈ ℕ0)
2927, 28syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘(𝑋 / )) ∈ ℕ0)
3029nn0cnd 12589 . . . . . . . . . 10 (𝜑 → (♯‘(𝑋 / )) ∈ ℂ)
31 eqid 2737 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
3231subg0cl 19152 . . . . . . . . . . . . . 14 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3317, 32syl 17 . . . . . . . . . . . . 13 (𝜑 → (0g𝐺) ∈ 𝐾)
3433ne0d 4342 . . . . . . . . . . . 12 (𝜑𝐾 ≠ ∅)
357subgss 19145 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3617, 35syl 17 . . . . . . . . . . . . . 14 (𝜑𝐾𝑋)
3710, 36ssfid 9301 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
38 hashnncl 14405 . . . . . . . . . . . . 13 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
3937, 38syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4034, 39mpbird 257 . . . . . . . . . . 11 (𝜑 → (♯‘𝐾) ∈ ℕ)
4140nncnd 12282 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ∈ ℂ)
4240nnne0d 12316 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ≠ 0)
4330, 41, 42divcan4d 12049 . . . . . . . . 9 (𝜑 → (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)) = (♯‘(𝑋 / )))
4419, 21, 433eqtr3d 2785 . . . . . . . 8 (𝜑 → ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (♯‘(𝑋 / )))
4544breq2d 5155 . . . . . . 7 (𝜑 → (𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ↔ 𝑃 ∥ (♯‘(𝑋 / ))))
4615, 45mtbid 324 . . . . . 6 (𝜑 → ¬ 𝑃 ∥ (♯‘(𝑋 / )))
47 prmz 16712 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
483, 47syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
4929nn0zd 12639 . . . . . . 7 (𝜑 → (♯‘(𝑋 / )) ∈ ℤ)
50 ssrab2 4080 . . . . . . . . . 10 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )
51 ssfi 9213 . . . . . . . . . 10 (((𝑋 / ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
5227, 50, 51sylancl 586 . . . . . . . . 9 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
53 hashcl 14395 . . . . . . . . 9 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5554nn0zd 12639 . . . . . . 7 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
56 eqid 2737 . . . . . . . 8 (Base‘(𝐺s 𝐻)) = (Base‘(𝐺s 𝐻))
57 sylow2b.a . . . . . . . . 9 + = (+g𝐺)
58 sylow2b.m . . . . . . . . 9 · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
597, 10, 4, 17, 57, 16, 58sylow2blem2 19639 . . . . . . . 8 (𝜑· ∈ ((𝐺s 𝐻) GrpAct (𝑋 / )))
60 eqid 2737 . . . . . . . . . . 11 (𝐺s 𝐻) = (𝐺s 𝐻)
6160subgbas 19148 . . . . . . . . . 10 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺s 𝐻)))
624, 61syl 17 . . . . . . . . 9 (𝜑𝐻 = (Base‘(𝐺s 𝐻)))
637subgss 19145 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻𝑋)
644, 63syl 17 . . . . . . . . . 10 (𝜑𝐻𝑋)
6510, 64ssfid 9301 . . . . . . . . 9 (𝜑𝐻 ∈ Fin)
6662, 65eqeltrrd 2842 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝐻)) ∈ Fin)
67 eqid 2737 . . . . . . . 8 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}
68 eqid 2737 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)}
6956, 59, 1, 66, 27, 67, 68sylow2a 19637 . . . . . . 7 (𝜑𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
70 dvdssub2 16338 . . . . . . 7 (((𝑃 ∈ ℤ ∧ (♯‘(𝑋 / )) ∈ ℤ ∧ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7148, 49, 55, 69, 70syl31anc 1375 . . . . . 6 (𝜑 → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7246, 71mtbid 324 . . . . 5 (𝜑 → ¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))
73 hasheq0 14402 . . . . . . . 8 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
7452, 73syl 17 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
75 dvds0 16309 . . . . . . . . 9 (𝑃 ∈ ℤ → 𝑃 ∥ 0)
7648, 75syl 17 . . . . . . . 8 (𝜑𝑃 ∥ 0)
77 breq2 5147 . . . . . . . 8 ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0))
7876, 77syl5ibrcom 247 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7974, 78sylbird 260 . . . . . 6 (𝜑 → ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
8079necon3bd 2954 . . . . 5 (𝜑 → (¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
8172, 80mpd 15 . . . 4 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
82 rabn0 4389 . . . 4 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8381, 82sylib 218 . . 3 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8462raleqdv 3326 . . . 4 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8584rexbidv 3179 . . 3 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8683, 85mpbird 257 . 2 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧)
87 vex 3484 . . . . 5 𝑧 ∈ V
8887elqs 8809 . . . 4 (𝑧 ∈ (𝑋 / ) ↔ ∃𝑔𝑋 𝑧 = [𝑔] )
89 simplrr 778 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] )
9089oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ))
91 simprr 773 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
92 simpll 767 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
93 simprl 771 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝐻)
94 simplrl 777 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔𝑋)
957, 10, 4, 17, 57, 16, 58sylow2blem1 19638 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝐻𝑔𝑋) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9692, 93, 94, 95syl3anc 1373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9790, 91, 963eqtr3d 2785 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] )
9889, 97eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] = [(𝑢 + 𝑔)] )
9925ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → Er 𝑋)
10099, 94erth 8796 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ [𝑔] = [(𝑢 + 𝑔)] ))
10198, 100mpbird 257 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 (𝑢 + 𝑔))
1026ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
10336ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾𝑋)
104 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (invg𝐺) = (invg𝐺)
1057, 104, 57, 16eqgval 19195 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐾𝑋) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
106102, 103, 105syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
107101, 106mpbid 232 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
108107simp3d 1145 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
109 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
110109oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) 𝑔) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
111 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) = (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))
112 ovex 7464 . . . . . . . . . . . . . . . . 17 ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) ∈ V
113110, 111, 112fvmpt 7016 . . . . . . . . . . . . . . . 16 ((((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
114108, 113syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
1157, 57, 31, 104grprinv 19008 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
116102, 94, 115syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
117116oveq1d 7446 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g𝐺) + (𝑢 + 𝑔)))
1187, 104grpinvcl 19005 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → ((invg𝐺)‘𝑔) ∈ 𝑋)
119102, 94, 118syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg𝐺)‘𝑔) ∈ 𝑋)
12064ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻𝑋)
121120, 93sseldd 3984 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝑋)
1227, 57grpcl 18959 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
123102, 121, 94, 122syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
1247, 57grpass 18960 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑔𝑋 ∧ ((invg𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
125102, 94, 119, 123, 124syl13anc 1374 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
1267, 57, 31grplid 18985 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
127102, 123, 126syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
128117, 125, 1273eqtr3d 2785 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
129128oveq1d 7446 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) = ((𝑢 + 𝑔) 𝑔))
130 sylow2blem3.d . . . . . . . . . . . . . . . . 17 = (-g𝐺)
1317, 57, 130grppncan 19049 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
132102, 121, 94, 131syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
133114, 129, 1323eqtrd 2781 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
134 ovex 7464 . . . . . . . . . . . . . . . 16 ((𝑔 + 𝑥) 𝑔) ∈ V
135134, 111fnmpti 6711 . . . . . . . . . . . . . . 15 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾
136 fnfvelrn 7100 . . . . . . . . . . . . . . 15 (((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
137135, 108, 136sylancr 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
138133, 137eqeltrrd 2842 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
139138expr 456 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ 𝑢𝐻) → ((𝑢 · 𝑧) = 𝑧𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
140139ralimdva 3167 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
141140imp 406 . . . . . . . . . 10 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
142141an32s 652 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
143 dfss3 3972 . . . . . . . . 9 (𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) ↔ ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
144142, 143sylibr 234 . . . . . . . 8 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
145144expr 456 . . . . . . 7 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔𝑋) → (𝑧 = [𝑔] 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
146145reximdva 3168 . . . . . 6 ((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
147146ex 412 . . . . 5 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
148147com23 86 . . . 4 (𝜑 → (∃𝑔𝑋 𝑧 = [𝑔] → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
14988, 148biimtrid 242 . . 3 (𝜑 → (𝑧 ∈ (𝑋 / ) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
150149rexlimdv 3153 . 2 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
15186, 150mpd 15 1 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  wss 3951  c0 4333  𝒫 cpw 4600  {cpr 4628   class class class wbr 5143  {copab 5205  cmpt 5225  ran crn 5686   Fn wfn 6556  cfv 6561  (class class class)co 7431  cmpo 7433   Er wer 8742  [cec 8743   / cqs 8744  Fincfn 8985  0cc0 11155   · cmul 11160  cmin 11492   / cdiv 11920  cn 12266  0cn0 12526  cz 12613  cexp 14102  chash 14369  cdvds 16290  cprime 16708   pCnt cpc 16874  Basecbs 17247  s cress 17274  +gcplusg 17297  0gc0g 17484  Grpcgrp 18951  invgcminusg 18952  -gcsg 18953  SubGrpcsubg 19138   ~QG cqg 19140   pGrp cpgp 19544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-omul 8511  df-er 8745  df-ec 8747  df-qs 8751  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-acn 9982  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-grp 18954  df-minusg 18955  df-sbg 18956  df-mulg 19086  df-subg 19141  df-eqg 19143  df-ga 19308  df-od 19546  df-pgp 19548
This theorem is referenced by:  sylow2b  19641
  Copyright terms: Public domain W3C validator