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

Theorem sylow3lem4 18807
 Description: Lemma for sylow3 18810, first part. The number of Sylow subgroups is a divisor of the size of 𝐺 reduced by the size of a Sylow subgroup of 𝐺. (Contributed by Mario Carneiro, 19-Jan-2015.)
Hypotheses
Ref Expression
sylow3.x 𝑋 = (Base‘𝐺)
sylow3.g (𝜑𝐺 ∈ Grp)
sylow3.xf (𝜑𝑋 ∈ Fin)
sylow3.p (𝜑𝑃 ∈ ℙ)
sylow3lem1.a + = (+g𝐺)
sylow3lem1.d = (-g𝐺)
sylow3lem1.m = (𝑥𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
sylow3lem2.k (𝜑𝐾 ∈ (𝑃 pSyl 𝐺))
sylow3lem2.h 𝐻 = {𝑢𝑋 ∣ (𝑢 𝐾) = 𝐾}
sylow3lem2.n 𝑁 = {𝑥𝑋 ∣ ∀𝑦𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
Assertion
Ref Expression
sylow3lem4 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
Distinct variable groups:   𝑥,𝑢,𝑦,𝑧,   𝑢, ,𝑥,𝑦,𝑧   𝑥,𝐻,𝑦   𝑢,𝐾,𝑥,𝑦,𝑧   𝑢,𝑁,𝑧   𝑢,𝑋,𝑥,𝑦,𝑧   𝑢,𝐺,𝑥,𝑦,𝑧   𝜑,𝑢,𝑥,𝑦,𝑧   𝑢, + ,𝑥,𝑦,𝑧   𝑢,𝑃,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐻(𝑧,𝑢)   𝑁(𝑥,𝑦)

Proof of Theorem sylow3lem4
StepHypRef Expression
1 sylow3.x . . 3 𝑋 = (Base‘𝐺)
2 sylow3.g . . 3 (𝜑𝐺 ∈ Grp)
3 sylow3.xf . . 3 (𝜑𝑋 ∈ Fin)
4 sylow3.p . . 3 (𝜑𝑃 ∈ ℙ)
5 sylow3lem1.a . . 3 + = (+g𝐺)
6 sylow3lem1.d . . 3 = (-g𝐺)
7 sylow3lem1.m . . 3 = (𝑥𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
8 sylow3lem2.k . . 3 (𝜑𝐾 ∈ (𝑃 pSyl 𝐺))
9 sylow3lem2.h . . 3 𝐻 = {𝑢𝑋 ∣ (𝑢 𝐾) = 𝐾}
10 sylow3lem2.n . . 3 𝑁 = {𝑥𝑋 ∣ ∀𝑦𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)}
111, 2, 3, 4, 5, 6, 7, 8, 9, 10sylow3lem3 18806 . 2 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~QG 𝑁))))
12 slwsubg 18787 . . . . . . . . . 10 (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
138, 12syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (SubGrp‘𝐺))
14 eqid 2759 . . . . . . . . . . 11 (𝐺s 𝑁) = (𝐺s 𝑁)
1510, 1, 5, 14nmznsg 18372 . . . . . . . . . 10 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)))
16 nsgsubg 18362 . . . . . . . . . 10 (𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1715, 16syl 17 . . . . . . . . 9 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1813, 17syl 17 . . . . . . . 8 (𝜑𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1910, 1, 5nmzsubg 18369 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
202, 19syl 17 . . . . . . . . . 10 (𝜑𝑁 ∈ (SubGrp‘𝐺))
2114subgbas 18335 . . . . . . . . . 10 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘(𝐺s 𝑁)))
2220, 21syl 17 . . . . . . . . 9 (𝜑𝑁 = (Base‘(𝐺s 𝑁)))
231subgss 18332 . . . . . . . . . . 11 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁𝑋)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝑁𝑋)
253, 24ssfid 8755 . . . . . . . . 9 (𝜑𝑁 ∈ Fin)
2622, 25eqeltrrd 2852 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝑁)) ∈ Fin)
27 eqid 2759 . . . . . . . . 9 (Base‘(𝐺s 𝑁)) = (Base‘(𝐺s 𝑁))
2827lagsubg 18394 . . . . . . . 8 ((𝐾 ∈ (SubGrp‘(𝐺s 𝑁)) ∧ (Base‘(𝐺s 𝑁)) ∈ Fin) → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
2918, 26, 28syl2anc 588 . . . . . . 7 (𝜑 → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
3022fveq2d 6655 . . . . . . 7 (𝜑 → (♯‘𝑁) = (♯‘(Base‘(𝐺s 𝑁))))
3129, 30breqtrrd 5053 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑁))
32 eqid 2759 . . . . . . . . . . . 12 (0g𝐺) = (0g𝐺)
3332subg0cl 18339 . . . . . . . . . . 11 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3413, 33syl 17 . . . . . . . . . 10 (𝜑 → (0g𝐺) ∈ 𝐾)
3534ne0d 4230 . . . . . . . . 9 (𝜑𝐾 ≠ ∅)
361subgss 18332 . . . . . . . . . . . 12 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3713, 36syl 17 . . . . . . . . . . 11 (𝜑𝐾𝑋)
383, 37ssfid 8755 . . . . . . . . . 10 (𝜑𝐾 ∈ Fin)
39 hashnncl 13762 . . . . . . . . . 10 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4038, 39syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4135, 40mpbird 260 . . . . . . . 8 (𝜑 → (♯‘𝐾) ∈ ℕ)
4241nnzd 12110 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℤ)
43 hashcl 13752 . . . . . . . . 9 (𝑁 ∈ Fin → (♯‘𝑁) ∈ ℕ0)
4425, 43syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑁) ∈ ℕ0)
4544nn0zd 12109 . . . . . . 7 (𝜑 → (♯‘𝑁) ∈ ℤ)
46 pwfi 8837 . . . . . . . . . . 11 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
473, 46sylib 221 . . . . . . . . . 10 (𝜑 → 𝒫 𝑋 ∈ Fin)
48 eqid 2759 . . . . . . . . . . . . 13 (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁)
491, 48eqger 18382 . . . . . . . . . . . 12 (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er 𝑋)
5020, 49syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺 ~QG 𝑁) Er 𝑋)
5150qsss 8361 . . . . . . . . . 10 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ⊆ 𝒫 𝑋)
5247, 51ssfid 8755 . . . . . . . . 9 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin)
53 hashcl 13752 . . . . . . . . 9 ((𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5554nn0zd 12109 . . . . . . 7 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ)
56 dvdscmul 15669 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝑁) ∈ ℤ ∧ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5742, 45, 55, 56syl3anc 1369 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5831, 57mpd 15 . . . . 5 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
59 hashcl 13752 . . . . . . . . 9 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
603, 59syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ0)
6160nn0cnd 11981 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℂ)
6241nncnd 11675 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℂ)
6341nnne0d 11709 . . . . . . 7 (𝜑 → (♯‘𝐾) ≠ 0)
6461, 62, 63divcan1d 11440 . . . . . 6 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = (♯‘𝑋))
651, 48, 20, 3lagsubg2 18393 . . . . . 6 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6664, 65eqtrd 2794 . . . . 5 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6758, 66breqtrrd 5053 . . . 4 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)))
681lagsubg 18394 . . . . . . 7 ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝐾) ∥ (♯‘𝑋))
6913, 3, 68syl2anc 588 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑋))
7060nn0zd 12109 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℤ)
71 dvdsval2 15643 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7242, 63, 70, 71syl3anc 1369 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7369, 72mpbid 235 . . . . 5 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ)
74 dvdsmulcr 15672 . . . . 5 (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ ∧ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ ∧ ((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0)) → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7555, 73, 42, 63, 74syl112anc 1372 . . . 4 (𝜑 → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7667, 75mpbid 235 . . 3 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾)))
771, 3, 8slwhash 18801 . . . 4 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
7877oveq2d 7159 . . 3 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
7976, 78breqtrd 5051 . 2 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
8011, 79eqbrtrd 5047 1 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539   ∈ wcel 2112   ≠ wne 2949  ∀wral 3068  {crab 3072   ⊆ wss 3854  ∅c0 4221  𝒫 cpw 4487   class class class wbr 5025   ↦ cmpt 5105  ran crn 5518  ‘cfv 6328  (class class class)co 7143   ∈ cmpo 7145   Er wer 8289   / cqs 8291  Fincfn 8520  0cc0 10560   · cmul 10565   / cdiv 11320  ℕcn 11659  ℕ0cn0 11919  ℤcz 12005  ↑cexp 13464  ♯chash 13725   ∥ cdvds 15640  ℙcprime 16052   pCnt cpc 16213  Basecbs 16526   ↾s cress 16527  +gcplusg 16608  0gc0g 16756  Grpcgrp 18154  -gcsg 18156  SubGrpcsubg 18325  NrmSGrpcnsg 18326   ~QG cqg 18327   pSyl cslw 18707 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-inf2 9122  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-pre-sup 10638 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-disj 4991  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-om 7573  df-1st 7686  df-2nd 7687  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-omul 8110  df-er 8292  df-ec 8294  df-qs 8298  df-map 8411  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-sup 8924  df-inf 8925  df-oi 8992  df-dju 9348  df-card 9386  df-acn 9389  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-div 11321  df-nn 11660  df-2 11722  df-3 11723  df-n0 11920  df-xnn0 11992  df-z 12006  df-uz 12268  df-q 12374  df-rp 12416  df-fz 12925  df-fzo 13068  df-fl 13196  df-mod 13272  df-seq 13404  df-exp 13465  df-fac 13669  df-bc 13698  df-hash 13726  df-cj 14491  df-re 14492  df-im 14493  df-sqrt 14627  df-abs 14628  df-clim 14878  df-sum 15076  df-dvds 15641  df-gcd 15879  df-prm 16053  df-pc 16214  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-0g 16758  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-submnd 18008  df-grp 18157  df-minusg 18158  df-sbg 18159  df-mulg 18277  df-subg 18328  df-nsg 18329  df-eqg 18330  df-ghm 18408  df-ga 18472  df-od 18708  df-pgp 18710  df-slw 18711 This theorem is referenced by:  sylow3  18810
 Copyright terms: Public domain W3C validator