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

Theorem sylow2blem3 18676
Description: Sylow's second theorem. Putting together the results of sylow2a 18673 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 18647 . . . . . . . . 9 (𝑃 pGrp (𝐺s 𝐻) → 𝑃 ∈ ℙ)
31, 2syl 17 . . . . . . . 8 (𝜑𝑃 ∈ ℙ)
4 sylow2b.h . . . . . . . . . . 11 (𝜑𝐻 ∈ (SubGrp‘𝐺))
5 subgrcl 18222 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
64, 5syl 17 . . . . . . . . . 10 (𝜑𝐺 ∈ Grp)
7 sylow2b.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
87grpbn0 18070 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝑋 ≠ ∅)
96, 8syl 17 . . . . . . . . 9 (𝜑𝑋 ≠ ∅)
10 sylow2b.xf . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
11 hashnncl 13715 . . . . . . . . . 10 (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1210, 11syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
139, 12mpbird 258 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ)
14 pcndvds2 16192 . . . . . . . 8 ((𝑃 ∈ ℙ ∧ (♯‘𝑋) ∈ ℕ) → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
153, 13, 14syl2anc 584 . . . . . . 7 (𝜑 → ¬ 𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
16 sylow2b.r . . . . . . . . . . 11 = (𝐺 ~QG 𝐾)
17 sylow2b.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (SubGrp‘𝐺))
187, 16, 17, 10lagsubg2 18279 . . . . . . . . . 10 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / )) · (♯‘𝐾)))
1918oveq1d 7160 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)))
20 sylow2blem3.kn . . . . . . . . . 10 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
2120oveq2d 7161 . . . . . . . . 9 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
22 pwfi 8807 . . . . . . . . . . . . . 14 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
2310, 22sylib 219 . . . . . . . . . . . . 13 (𝜑 → 𝒫 𝑋 ∈ Fin)
247, 16eqger 18268 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → Er 𝑋)
2517, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 Er 𝑋)
2625qsss 8347 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / ) ⊆ 𝒫 𝑋)
2723, 26ssfid 8729 . . . . . . . . . . . 12 (𝜑 → (𝑋 / ) ∈ Fin)
28 hashcl 13705 . . . . . . . . . . . 12 ((𝑋 / ) ∈ Fin → (♯‘(𝑋 / )) ∈ ℕ0)
2927, 28syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘(𝑋 / )) ∈ ℕ0)
3029nn0cnd 11945 . . . . . . . . . 10 (𝜑 → (♯‘(𝑋 / )) ∈ ℂ)
31 eqid 2818 . . . . . . . . . . . . . . 15 (0g𝐺) = (0g𝐺)
3231subg0cl 18225 . . . . . . . . . . . . . 14 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3317, 32syl 17 . . . . . . . . . . . . 13 (𝜑 → (0g𝐺) ∈ 𝐾)
3433ne0d 4298 . . . . . . . . . . . 12 (𝜑𝐾 ≠ ∅)
357subgss 18218 . . . . . . . . . . . . . . 15 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3617, 35syl 17 . . . . . . . . . . . . . 14 (𝜑𝐾𝑋)
3710, 36ssfid 8729 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ Fin)
38 hashnncl 13715 . . . . . . . . . . . . 13 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
3937, 38syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4034, 39mpbird 258 . . . . . . . . . . 11 (𝜑 → (♯‘𝐾) ∈ ℕ)
4140nncnd 11642 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ∈ ℂ)
4240nnne0d 11675 . . . . . . . . . 10 (𝜑 → (♯‘𝐾) ≠ 0)
4330, 41, 42divcan4d 11410 . . . . . . . . 9 (𝜑 → (((♯‘(𝑋 / )) · (♯‘𝐾)) / (♯‘𝐾)) = (♯‘(𝑋 / )))
4419, 21, 433eqtr3d 2861 . . . . . . . 8 (𝜑 → ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) = (♯‘(𝑋 / )))
4544breq2d 5069 . . . . . . 7 (𝜑 → (𝑃 ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))) ↔ 𝑃 ∥ (♯‘(𝑋 / ))))
4615, 45mtbid 325 . . . . . 6 (𝜑 → ¬ 𝑃 ∥ (♯‘(𝑋 / )))
47 prmz 16007 . . . . . . . 8 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
483, 47syl 17 . . . . . . 7 (𝜑𝑃 ∈ ℤ)
4929nn0zd 12073 . . . . . . 7 (𝜑 → (♯‘(𝑋 / )) ∈ ℤ)
50 ssrab2 4053 . . . . . . . . . 10 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )
51 ssfi 8726 . . . . . . . . . 10 (((𝑋 / ) ∈ Fin ∧ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ⊆ (𝑋 / )) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
5227, 50, 51sylancl 586 . . . . . . . . 9 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin)
53 hashcl 13705 . . . . . . . . 9 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℕ0)
5554nn0zd 12073 . . . . . . 7 (𝜑 → (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ)
56 eqid 2818 . . . . . . . 8 (Base‘(𝐺s 𝐻)) = (Base‘(𝐺s 𝐻))
57 sylow2b.a . . . . . . . . 9 + = (+g𝐺)
58 sylow2b.m . . . . . . . . 9 · = (𝑥𝐻, 𝑦 ∈ (𝑋 / ) ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
597, 10, 4, 17, 57, 16, 58sylow2blem2 18675 . . . . . . . 8 (𝜑· ∈ ((𝐺s 𝐻) GrpAct (𝑋 / )))
60 eqid 2818 . . . . . . . . . . 11 (𝐺s 𝐻) = (𝐺s 𝐻)
6160subgbas 18221 . . . . . . . . . 10 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 = (Base‘(𝐺s 𝐻)))
624, 61syl 17 . . . . . . . . 9 (𝜑𝐻 = (Base‘(𝐺s 𝐻)))
637subgss 18218 . . . . . . . . . . 11 (𝐻 ∈ (SubGrp‘𝐺) → 𝐻𝑋)
644, 63syl 17 . . . . . . . . . 10 (𝜑𝐻𝑋)
6510, 64ssfid 8729 . . . . . . . . 9 (𝜑𝐻 ∈ Fin)
6662, 65eqeltrrd 2911 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝐻)) ∈ Fin)
67 eqid 2818 . . . . . . . 8 {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}
68 eqid 2818 . . . . . . . 8 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (𝑋 / ) ∧ ∃𝑔 ∈ (Base‘(𝐺s 𝐻))(𝑔 · 𝑥) = 𝑦)}
6956, 59, 1, 66, 27, 67, 68sylow2a 18673 . . . . . . 7 (𝜑𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
70 dvdssub2 15639 . . . . . . 7 (((𝑃 ∈ ℤ ∧ (♯‘(𝑋 / )) ∈ ℤ ∧ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ∈ ℤ) ∧ 𝑃 ∥ ((♯‘(𝑋 / )) − (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))) → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7148, 49, 55, 69, 70syl31anc 1365 . . . . . 6 (𝜑 → (𝑃 ∥ (♯‘(𝑋 / )) ↔ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7246, 71mtbid 325 . . . . 5 (𝜑 → ¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}))
73 hasheq0 13712 . . . . . . . 8 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ∈ Fin → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
7452, 73syl 17 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 ↔ {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅))
75 dvds0 15613 . . . . . . . . 9 (𝑃 ∈ ℤ → 𝑃 ∥ 0)
7648, 75syl 17 . . . . . . . 8 (𝜑𝑃 ∥ 0)
77 breq2 5061 . . . . . . . 8 ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → (𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) ↔ 𝑃 ∥ 0))
7876, 77syl5ibrcom 248 . . . . . . 7 (𝜑 → ((♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) = 0 → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
7974, 78sylbird 261 . . . . . 6 (𝜑 → ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} = ∅ → 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧})))
8079necon3bd 3027 . . . . 5 (𝜑 → (¬ 𝑃 ∥ (♯‘{𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧}) → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅))
8172, 80mpd 15 . . . 4 (𝜑 → {𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅)
82 rabn0 4336 . . . 4 ({𝑧 ∈ (𝑋 / ) ∣ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧} ≠ ∅ ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8381, 82sylib 219 . . 3 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧)
8462raleqdv 3413 . . . 4 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8584rexbidv 3294 . . 3 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 ↔ ∃𝑧 ∈ (𝑋 / )∀𝑢 ∈ (Base‘(𝐺s 𝐻))(𝑢 · 𝑧) = 𝑧))
8683, 85mpbird 258 . 2 (𝜑 → ∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧)
87 vex 3495 . . . . 5 𝑧 ∈ V
8887elqs 8338 . . . 4 (𝑧 ∈ (𝑋 / ) ↔ ∃𝑔𝑋 𝑧 = [𝑔] )
89 simplrr 774 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [𝑔] )
9089oveq2d 7161 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = (𝑢 · [𝑔] ))
91 simprr 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · 𝑧) = 𝑧)
92 simpll 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝜑)
93 simprl 767 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝐻)
94 simplrl 773 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔𝑋)
957, 10, 4, 17, 57, 16, 58sylow2blem1 18674 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑢𝐻𝑔𝑋) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9692, 93, 94, 95syl3anc 1363 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 · [𝑔] ) = [(𝑢 + 𝑔)] )
9790, 91, 963eqtr3d 2861 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑧 = [(𝑢 + 𝑔)] )
9889, 97eqtr3d 2855 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → [𝑔] = [(𝑢 + 𝑔)] )
9925ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → Er 𝑋)
10099, 94erth 8327 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ [𝑔] = [(𝑢 + 𝑔)] ))
10198, 100mpbird 258 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑔 (𝑢 + 𝑔))
1026ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐺 ∈ Grp)
10336ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐾𝑋)
104 eqid 2818 . . . . . . . . . . . . . . . . . . . 20 (invg𝐺) = (invg𝐺)
1057, 104, 57, 16eqgval 18267 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝐾𝑋) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
106102, 103, 105syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 (𝑢 + 𝑔) ↔ (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)))
107101, 106mpbid 233 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾))
108107simp3d 1136 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾)
109 oveq2 7153 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → (𝑔 + 𝑥) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
110109oveq1d 7160 . . . . . . . . . . . . . . . . 17 (𝑥 = (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) → ((𝑔 + 𝑥) 𝑔) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
111 eqid 2818 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) = (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))
112 ovex 7178 . . . . . . . . . . . . . . . . 17 ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) ∈ V
113110, 111, 112fvmpt 6761 . . . . . . . . . . . . . . . 16 ((((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾 → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
114108, 113syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔))
1157, 57, 31, 104grprinv 18091 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
116102, 94, 115syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + ((invg𝐺)‘𝑔)) = (0g𝐺))
117116oveq1d 7160 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = ((0g𝐺) + (𝑢 + 𝑔)))
1187, 104grpinvcl 18089 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑔𝑋) → ((invg𝐺)‘𝑔) ∈ 𝑋)
119102, 94, 118syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((invg𝐺)‘𝑔) ∈ 𝑋)
12064ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝐻𝑋)
121120, 93sseldd 3965 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢𝑋)
1227, 57grpcl 18049 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → (𝑢 + 𝑔) ∈ 𝑋)
123102, 121, 94, 122syl3anc 1363 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑢 + 𝑔) ∈ 𝑋)
1247, 57grpass 18050 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑔𝑋 ∧ ((invg𝐺)‘𝑔) ∈ 𝑋 ∧ (𝑢 + 𝑔) ∈ 𝑋)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
125102, 94, 119, 123, 124syl13anc 1364 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + ((invg𝐺)‘𝑔)) + (𝑢 + 𝑔)) = (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))))
1267, 57, 31grplid 18071 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (𝑢 + 𝑔) ∈ 𝑋) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
127102, 123, 126syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((0g𝐺) + (𝑢 + 𝑔)) = (𝑢 + 𝑔))
128117, 125, 1273eqtr3d 2861 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → (𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = (𝑢 + 𝑔))
129128oveq1d 7160 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑔 + (((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) 𝑔) = ((𝑢 + 𝑔) 𝑔))
130 sylow2blem3.d . . . . . . . . . . . . . . . . 17 = (-g𝐺)
1317, 57, 130grppncan 18128 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ 𝑢𝑋𝑔𝑋) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
132102, 121, 94, 131syl3anc 1363 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑢 + 𝑔) 𝑔) = 𝑢)
133114, 129, 1323eqtrd 2857 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) = 𝑢)
134 ovex 7178 . . . . . . . . . . . . . . . 16 ((𝑔 + 𝑥) 𝑔) ∈ V
135134, 111fnmpti 6484 . . . . . . . . . . . . . . 15 (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾
136 fnfvelrn 6840 . . . . . . . . . . . . . . 15 (((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) Fn 𝐾 ∧ (((invg𝐺)‘𝑔) + (𝑢 + 𝑔)) ∈ 𝐾) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
137135, 108, 136sylancr 587 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → ((𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))‘(((invg𝐺)‘𝑔) + (𝑢 + 𝑔))) ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
138133, 137eqeltrrd 2911 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ (𝑢𝐻 ∧ (𝑢 · 𝑧) = 𝑧)) → 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
139138expr 457 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ 𝑢𝐻) → ((𝑢 · 𝑧) = 𝑧𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
140139ralimdva 3174 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
141140imp 407 . . . . . . . . . 10 (((𝜑 ∧ (𝑔𝑋𝑧 = [𝑔] )) ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
142141an32s 648 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
143 dfss3 3953 . . . . . . . . 9 (𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)) ↔ ∀𝑢𝐻 𝑢 ∈ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
144142, 143sylibr 235 . . . . . . . 8 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ (𝑔𝑋𝑧 = [𝑔] )) → 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
145144expr 457 . . . . . . 7 (((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) ∧ 𝑔𝑋) → (𝑧 = [𝑔] 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
146145reximdva 3271 . . . . . 6 ((𝜑 ∧ ∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧) → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
147146ex 413 . . . . 5 (𝜑 → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → (∃𝑔𝑋 𝑧 = [𝑔] → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
148147com23 86 . . . 4 (𝜑 → (∃𝑔𝑋 𝑧 = [𝑔] → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
14988, 148syl5bi 243 . . 3 (𝜑 → (𝑧 ∈ (𝑋 / ) → (∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))))
150149rexlimdv 3280 . 2 (𝜑 → (∃𝑧 ∈ (𝑋 / )∀𝑢𝐻 (𝑢 · 𝑧) = 𝑧 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔))))
15186, 150mpd 15 1 (𝜑 → ∃𝑔𝑋 𝐻 ⊆ ran (𝑥𝐾 ↦ ((𝑔 + 𝑥) 𝑔)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  wss 3933  c0 4288  𝒫 cpw 4535  {cpr 4559   class class class wbr 5057  {copab 5119  cmpt 5137  ran crn 5549   Fn wfn 6343  cfv 6348  (class class class)co 7145  cmpo 7147   Er wer 8275  [cec 8276   / cqs 8277  Fincfn 8497  0cc0 10525   · cmul 10530  cmin 10858   / cdiv 11285  cn 11626  0cn0 11885  cz 11969  cexp 13417  chash 13678  cdvds 15595  cprime 16003   pCnt cpc 16161  Basecbs 16471  s cress 16472  +gcplusg 16553  0gc0g 16701  Grpcgrp 18041  invgcminusg 18042  -gcsg 18043  SubGrpcsubg 18211   ~QG cqg 18213   pGrp cpgp 18583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-er 8278  df-ec 8280  df-qs 8284  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-sum 15031  df-dvds 15596  df-gcd 15832  df-prm 16004  df-pc 16162  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-0g 16703  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-grp 18044  df-minusg 18045  df-sbg 18046  df-mulg 18163  df-subg 18214  df-eqg 18216  df-ga 18358  df-od 18585  df-pgp 18587
This theorem is referenced by:  sylow2b  18677
  Copyright terms: Public domain W3C validator