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

Theorem sylow3lem4 19663
Description: Lemma for sylow3 19666, 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 19662 . 2 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~QG 𝑁))))
12 slwsubg 19643 . . . . . . . . . 10 (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
138, 12syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (SubGrp‘𝐺))
14 eqid 2735 . . . . . . . . . . 11 (𝐺s 𝑁) = (𝐺s 𝑁)
1510, 1, 5, 14nmznsg 19199 . . . . . . . . . 10 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)))
16 nsgsubg 19189 . . . . . . . . . 10 (𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1715, 16syl 17 . . . . . . . . 9 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1813, 17syl 17 . . . . . . . 8 (𝜑𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1910, 1, 5nmzsubg 19196 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
202, 19syl 17 . . . . . . . . . 10 (𝜑𝑁 ∈ (SubGrp‘𝐺))
2114subgbas 19161 . . . . . . . . . 10 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘(𝐺s 𝑁)))
2220, 21syl 17 . . . . . . . . 9 (𝜑𝑁 = (Base‘(𝐺s 𝑁)))
231subgss 19158 . . . . . . . . . . 11 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁𝑋)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝑁𝑋)
253, 24ssfid 9299 . . . . . . . . 9 (𝜑𝑁 ∈ Fin)
2622, 25eqeltrrd 2840 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝑁)) ∈ Fin)
27 eqid 2735 . . . . . . . . 9 (Base‘(𝐺s 𝑁)) = (Base‘(𝐺s 𝑁))
2827lagsubg 19226 . . . . . . . 8 ((𝐾 ∈ (SubGrp‘(𝐺s 𝑁)) ∧ (Base‘(𝐺s 𝑁)) ∈ Fin) → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
2918, 26, 28syl2anc 584 . . . . . . 7 (𝜑 → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
3022fveq2d 6911 . . . . . . 7 (𝜑 → (♯‘𝑁) = (♯‘(Base‘(𝐺s 𝑁))))
3129, 30breqtrrd 5176 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑁))
32 eqid 2735 . . . . . . . . . . . 12 (0g𝐺) = (0g𝐺)
3332subg0cl 19165 . . . . . . . . . . 11 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3413, 33syl 17 . . . . . . . . . 10 (𝜑 → (0g𝐺) ∈ 𝐾)
3534ne0d 4348 . . . . . . . . 9 (𝜑𝐾 ≠ ∅)
361subgss 19158 . . . . . . . . . . . 12 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3713, 36syl 17 . . . . . . . . . . 11 (𝜑𝐾𝑋)
383, 37ssfid 9299 . . . . . . . . . 10 (𝜑𝐾 ∈ Fin)
39 hashnncl 14402 . . . . . . . . . 10 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4038, 39syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4135, 40mpbird 257 . . . . . . . 8 (𝜑 → (♯‘𝐾) ∈ ℕ)
4241nnzd 12638 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℤ)
43 hashcl 14392 . . . . . . . . 9 (𝑁 ∈ Fin → (♯‘𝑁) ∈ ℕ0)
4425, 43syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑁) ∈ ℕ0)
4544nn0zd 12637 . . . . . . 7 (𝜑 → (♯‘𝑁) ∈ ℤ)
46 pwfi 9355 . . . . . . . . . . 11 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
473, 46sylib 218 . . . . . . . . . 10 (𝜑 → 𝒫 𝑋 ∈ Fin)
48 eqid 2735 . . . . . . . . . . . . 13 (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁)
491, 48eqger 19209 . . . . . . . . . . . 12 (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er 𝑋)
5020, 49syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺 ~QG 𝑁) Er 𝑋)
5150qsss 8817 . . . . . . . . . 10 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ⊆ 𝒫 𝑋)
5247, 51ssfid 9299 . . . . . . . . 9 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin)
53 hashcl 14392 . . . . . . . . 9 ((𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5554nn0zd 12637 . . . . . . 7 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ)
56 dvdscmul 16317 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝑁) ∈ ℤ ∧ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5742, 45, 55, 56syl3anc 1370 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5831, 57mpd 15 . . . . 5 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
59 hashcl 14392 . . . . . . . . 9 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
603, 59syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ0)
6160nn0cnd 12587 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℂ)
6241nncnd 12280 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℂ)
6341nnne0d 12314 . . . . . . 7 (𝜑 → (♯‘𝐾) ≠ 0)
6461, 62, 63divcan1d 12042 . . . . . 6 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = (♯‘𝑋))
651, 48, 20, 3lagsubg2 19225 . . . . . 6 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6664, 65eqtrd 2775 . . . . 5 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6758, 66breqtrrd 5176 . . . 4 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)))
681lagsubg 19226 . . . . . . 7 ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝐾) ∥ (♯‘𝑋))
6913, 3, 68syl2anc 584 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑋))
7060nn0zd 12637 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℤ)
71 dvdsval2 16290 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7242, 63, 70, 71syl3anc 1370 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7369, 72mpbid 232 . . . . 5 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ)
74 dvdsmulcr 16320 . . . . 5 (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ ∧ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ ∧ ((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0)) → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7555, 73, 42, 63, 74syl112anc 1373 . . . 4 (𝜑 → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7667, 75mpbid 232 . . 3 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾)))
771, 3, 8slwhash 19657 . . . 4 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
7877oveq2d 7447 . . 3 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
7976, 78breqtrd 5174 . 2 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
8011, 79eqbrtrd 5170 1 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wcel 2106  wne 2938  wral 3059  {crab 3433  wss 3963  c0 4339  𝒫 cpw 4605   class class class wbr 5148  cmpt 5231  ran crn 5690  cfv 6563  (class class class)co 7431  cmpo 7433   Er wer 8741   / cqs 8743  Fincfn 8984  0cc0 11153   · cmul 11158   / cdiv 11918  cn 12264  0cn0 12524  cz 12611  cexp 14099  chash 14366  cdvds 16287  cprime 16705   pCnt cpc 16870  Basecbs 17245  s cress 17274  +gcplusg 17298  0gc0g 17486  Grpcgrp 18964  -gcsg 18966  SubGrpcsubg 19151  NrmSGrpcnsg 19152   ~QG cqg 19153   pSyl cslw 19560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-omul 8510  df-er 8744  df-ec 8746  df-qs 8750  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-acn 9980  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12598  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-fac 14310  df-bc 14339  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-sum 15720  df-dvds 16288  df-gcd 16529  df-prm 16706  df-pc 16871  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-subg 19154  df-nsg 19155  df-eqg 19156  df-ghm 19244  df-ga 19321  df-od 19561  df-pgp 19563  df-slw 19564
This theorem is referenced by:  sylow3  19666
  Copyright terms: Public domain W3C validator