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

Theorem sylow2blem3 19404
Description: Sylow's second theorem. Putting together the results of sylow2a 19401 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 19375 . . . . . . . . 9 (𝑃 pGrp (𝐺s 𝐻) → 𝑃 ∈ ℙ)
31, 2syl 17 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
4 sylow2b.h . . . . . . . . . . 11 (𝜑𝐻 ∈ (SubGrp‘𝐺))
5 subgrcl 18933 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
7 sylow2b.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
87grpbn0 18779 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
96, 8syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
10 sylow2b.xf . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
11 hashnncl 14266 . . . . . . . . . 10 (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1210, 11syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
139, 12mpbird 256 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ)
14 pcndvds2 16740 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (♯‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
153, 13, 14syl2anc 584 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
16 sylow2b.r . . . . . . . . . . 11 = (𝐺 ~QG 𝐾)
17 sylow2b.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (SubGrp‘𝐺))
187, 16, 17, 10lagsubg2 18991 . . . . . . . . . 10 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / )) · (♯‘𝐾)))
1918oveq1d 7372 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)))
20 sylow2blem3.kn . . . . . . . . . 10 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
2120oveq2d 7373 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
22 pwfi 9122 . . . . . . . . . . . . . 14 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
2310, 22sylib 217 . . . . . . . . . . . . 13 (𝜑 → 𝒫 𝑋 ∈ Fin)
247, 16eqger 18980 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → Er 𝑋)
2517, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 Er 𝑋)
2625qsss 8717 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / ) ⊆ 𝒫 𝑋)
2723, 26ssfid 9211 . . . . . . . . . . . 12 (𝜑 → (𝑋 / ) ∈ Fin)
28 hashcl 14256 . . . . . . . . . . . 12 ((𝑋 / ) ∈ Fin → (♯‘(𝑋 / )) ∈ ℕ0)
2927, 28syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘(𝑋 / )) ∈ ℕ0)
3029nn0cnd 12475 . . . . . . . . . 10 (𝜑 → (♯‘(𝑋 / )) ∈ ℂ)
31 eqid 2736 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
3231subg0cl 18936 . . . . . . . . . . . . . 14 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3317, 32syl 17 . . . . . . . . . . . . 13 (𝜑 → (0g𝐺) ∈ 𝐾)
3433ne0d 4295 . . . . . . . . . . . 12 (𝜑𝐾 ≠ ∅)
357subgss 18929 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3617, 35syl 17 . . . . . . . . . . . . . 14 (𝜑𝐾𝑋)
3710, 36ssfid 9211 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
38 hashnncl 14266 . . . . . . . . . . . . 13 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
3937, 38syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4034, 39mpbird 256 . . . . . . . . . . 11 (𝜑 → (♯‘𝐾) ∈ ℕ)
4140nncnd 12169 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ∈ ℂ)
4240nnne0d 12203 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ≠ 0)
4330, 41, 42divcan4d 11937 . . . . . . . . 9 (𝜑 → (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)) = (♯‘(𝑋 / )))
4419, 21, 433eqtr3d 2784 . . . . . . . 8 (𝜑 → ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (♯‘(𝑋 / )))
4544breq2d 5117 . . . . . . 7 (𝜑 → (𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ↔ 𝑃 ∥ (♯‘(𝑋 / ))))
4615, 45mtbid 323 . . . . . 6 (𝜑 → ¬ 𝑃 ∥ (♯‘(𝑋 / )))
47 prmz 16551 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
483, 47syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
4929nn0zd 12525 . . . . . . 7 (𝜑 → (♯‘(𝑋 / )) ∈ ℤ)
50 ssrab2 4037 . . . . . . . . . 10 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )
51 ssfi 9117 . . . . . . . . . 10 (((𝑋 / ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
5227, 50, 51sylancl 586 . . . . . . . . 9 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
53 hashcl 14256 . . . . . . . . 9 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5554nn0zd 12525 . . . . . . 7 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
56 eqid 2736 . . . . . . . 8 (Base‘(𝐺s 𝐻)) = (Base‘(𝐺s 𝐻))
57 sylow2b.a . . . . . . . . 9 + = (+g𝐺)
58 sylow2b.m . . . . . . . . 9 · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
597, 10, 4, 17, 57, 16, 58sylow2blem2 19403 . . . . . . . 8 (𝜑· ∈ ((𝐺s 𝐻) GrpAct (𝑋 / )))
60 eqid 2736 . . . . . . . . . . 11 (𝐺s 𝐻) = (𝐺s 𝐻)
6160subgbas 18932 . . . . . . . . . 10 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺s 𝐻)))
624, 61syl 17 . . . . . . . . 9 (𝜑𝐻 = (Base‘(𝐺s 𝐻)))
637subgss 18929 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻𝑋)
644, 63syl 17 . . . . . . . . . 10 (𝜑𝐻𝑋)
6510, 64ssfid 9211 . . . . . . . . 9 (𝜑𝐻 ∈ Fin)
6662, 65eqeltrrd 2839 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝐻)) ∈ Fin)
67 eqid 2736 . . . . . . . 8 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}
68 eqid 2736 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)}
6956, 59, 1, 66, 27, 67, 68sylow2a 19401 . . . . . . 7 (𝜑𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
70 dvdssub2 16183 . . . . . . 7 (((𝑃 ∈ ℤ ∧ (♯‘(𝑋 / )) ∈ ℤ ∧ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7148, 49, 55, 69, 70syl31anc 1373 . . . . . 6 (𝜑 → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7246, 71mtbid 323 . . . . 5 (𝜑 → ¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))
73 hasheq0 14263 . . . . . . . 8 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
7452, 73syl 17 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
75 dvds0 16154 . . . . . . . . 9 (𝑃 ∈ ℤ → 𝑃 ∥ 0)
7648, 75syl 17 . . . . . . . 8 (𝜑𝑃 ∥ 0)
77 breq2 5109 . . . . . . . 8 ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0))
7876, 77syl5ibrcom 246 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7974, 78sylbird 259 . . . . . 6 (𝜑 → ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
8079necon3bd 2957 . . . . 5 (𝜑 → (¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
8172, 80mpd 15 . . . 4 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
82 rabn0 4345 . . . 4 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8381, 82sylib 217 . . 3 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8462raleqdv 3313 . . . 4 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8584rexbidv 3175 . . 3 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8683, 85mpbird 256 . 2 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧)
87 vex 3449 . . . . 5 𝑧 ∈ V
8887elqs 8708 . . . 4 (𝑧 ∈ (𝑋 / ) ↔ ∃𝑔𝑋 𝑧 = [𝑔] )
89 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] )
9089oveq2d 7373 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ))
91 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
92 simpll 765 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
93 simprl 769 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝐻)
94 simplrl 775 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔𝑋)
957, 10, 4, 17, 57, 16, 58sylow2blem1 19402 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝐻𝑔𝑋) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9692, 93, 94, 95syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9790, 91, 963eqtr3d 2784 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] )
9889, 97eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] = [(𝑢 + 𝑔)] )
9925ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → Er 𝑋)
10099, 94erth 8697 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ [𝑔] = [(𝑢 + 𝑔)] ))
10198, 100mpbird 256 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 (𝑢 + 𝑔))
1026ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
10336ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾𝑋)
104 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (invg𝐺) = (invg𝐺)
1057, 104, 57, 16eqgval 18979 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐾𝑋) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
106102, 103, 105syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
107101, 106mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
108107simp3d 1144 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
109 oveq2 7365 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
110109oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) 𝑔) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
111 eqid 2736 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) = (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))
112 ovex 7390 . . . . . . . . . . . . . . . . 17 ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) ∈ V
113110, 111, 112fvmpt 6948 . . . . . . . . . . . . . . . 16 ((((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
114108, 113syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
1157, 57, 31, 104grprinv 18801 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
116102, 94, 115syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
117116oveq1d 7372 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g𝐺) + (𝑢 + 𝑔)))
1187, 104grpinvcl 18798 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → ((invg𝐺)‘𝑔) ∈ 𝑋)
119102, 94, 118syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg𝐺)‘𝑔) ∈ 𝑋)
12064ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻𝑋)
121120, 93sseldd 3945 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝑋)
1227, 57grpcl 18756 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
123102, 121, 94, 122syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
1247, 57grpass 18757 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑔𝑋 ∧ ((invg𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
125102, 94, 119, 123, 124syl13anc 1372 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
1267, 57, 31grplid 18780 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
127102, 123, 126syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
128117, 125, 1273eqtr3d 2784 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
129128oveq1d 7372 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) = ((𝑢 + 𝑔) 𝑔))
130 sylow2blem3.d . . . . . . . . . . . . . . . . 17 = (-g𝐺)
1317, 57, 130grppncan 18838 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
132102, 121, 94, 131syl3anc 1371 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
133114, 129, 1323eqtrd 2780 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
134 ovex 7390 . . . . . . . . . . . . . . . 16 ((𝑔 + 𝑥) 𝑔) ∈ V
135134, 111fnmpti 6644 . . . . . . . . . . . . . . 15 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾
136 fnfvelrn 7031 . . . . . . . . . . . . . . 15 (((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
137135, 108, 136sylancr 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
138133, 137eqeltrrd 2839 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
139138expr 457 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ 𝑢𝐻) → ((𝑢 · 𝑧) = 𝑧𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
140139ralimdva 3164 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
141140imp 407 . . . . . . . . . 10 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
142141an32s 650 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
143 dfss3 3932 . . . . . . . . 9 (𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) ↔ ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
144142, 143sylibr 233 . . . . . . . 8 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
145144expr 457 . . . . . . 7 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔𝑋) → (𝑧 = [𝑔] 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
146145reximdva 3165 . . . . . 6 ((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
147146ex 413 . . . . 5 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
148147com23 86 . . . 4 (𝜑 → (∃𝑔𝑋 𝑧 = [𝑔] → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
14988, 148biimtrid 241 . . 3 (𝜑 → (𝑧 ∈ (𝑋 / ) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
150149rexlimdv 3150 . 2 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
15186, 150mpd 15 1 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  wss 3910  c0 4282  𝒫 cpw 4560  {cpr 4588   class class class wbr 5105  {copab 5167  cmpt 5188  ran crn 5634   Fn wfn 6491  cfv 6496  (class class class)co 7357  cmpo 7359   Er wer 8645  [cec 8646   / cqs 8647  Fincfn 8883  0cc0 11051   · cmul 11056  cmin 11385   / cdiv 11812  cn 12153  0cn0 12413  cz 12499  cexp 13967  chash 14230  cdvds 16136  cprime 16547   pCnt cpc 16708  Basecbs 17083  s cress 17112  +gcplusg 17133  0gc0g 17321  Grpcgrp 18748  invgcminusg 18749  -gcsg 18750  SubGrpcsubg 18922   ~QG cqg 18924   pGrp cpgp 19308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-ec 8650  df-qs 8654  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-dvds 16137  df-gcd 16375  df-prm 16548  df-pc 16709  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-eqg 18927  df-ga 19070  df-od 19310  df-pgp 19312
This theorem is referenced by:  sylow2b  19405
  Copyright terms: Public domain W3C validator