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

Theorem sylow3lem4 19648
Description: Lemma for sylow3 19651, 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 19647 . 2 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) = (♯‘(𝑋 / (𝐺 ~QG 𝑁))))
12 slwsubg 19628 . . . . . . . . . 10 (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺))
138, 12syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ (SubGrp‘𝐺))
14 eqid 2737 . . . . . . . . . . 11 (𝐺s 𝑁) = (𝐺s 𝑁)
1510, 1, 5, 14nmznsg 19186 . . . . . . . . . 10 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)))
16 nsgsubg 19176 . . . . . . . . . 10 (𝐾 ∈ (NrmSGrp‘(𝐺s 𝑁)) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1715, 16syl 17 . . . . . . . . 9 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1813, 17syl 17 . . . . . . . 8 (𝜑𝐾 ∈ (SubGrp‘(𝐺s 𝑁)))
1910, 1, 5nmzsubg 19183 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
202, 19syl 17 . . . . . . . . . 10 (𝜑𝑁 ∈ (SubGrp‘𝐺))
2114subgbas 19148 . . . . . . . . . 10 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘(𝐺s 𝑁)))
2220, 21syl 17 . . . . . . . . 9 (𝜑𝑁 = (Base‘(𝐺s 𝑁)))
231subgss 19145 . . . . . . . . . . 11 (𝑁 ∈ (SubGrp‘𝐺) → 𝑁𝑋)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝑁𝑋)
253, 24ssfid 9301 . . . . . . . . 9 (𝜑𝑁 ∈ Fin)
2622, 25eqeltrrd 2842 . . . . . . . 8 (𝜑 → (Base‘(𝐺s 𝑁)) ∈ Fin)
27 eqid 2737 . . . . . . . . 9 (Base‘(𝐺s 𝑁)) = (Base‘(𝐺s 𝑁))
2827lagsubg 19213 . . . . . . . 8 ((𝐾 ∈ (SubGrp‘(𝐺s 𝑁)) ∧ (Base‘(𝐺s 𝑁)) ∈ Fin) → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
2918, 26, 28syl2anc 584 . . . . . . 7 (𝜑 → (♯‘𝐾) ∥ (♯‘(Base‘(𝐺s 𝑁))))
3022fveq2d 6910 . . . . . . 7 (𝜑 → (♯‘𝑁) = (♯‘(Base‘(𝐺s 𝑁))))
3129, 30breqtrrd 5171 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑁))
32 eqid 2737 . . . . . . . . . . . 12 (0g𝐺) = (0g𝐺)
3332subg0cl 19152 . . . . . . . . . . 11 (𝐾 ∈ (SubGrp‘𝐺) → (0g𝐺) ∈ 𝐾)
3413, 33syl 17 . . . . . . . . . 10 (𝜑 → (0g𝐺) ∈ 𝐾)
3534ne0d 4342 . . . . . . . . 9 (𝜑𝐾 ≠ ∅)
361subgss 19145 . . . . . . . . . . . 12 (𝐾 ∈ (SubGrp‘𝐺) → 𝐾𝑋)
3713, 36syl 17 . . . . . . . . . . 11 (𝜑𝐾𝑋)
383, 37ssfid 9301 . . . . . . . . . 10 (𝜑𝐾 ∈ Fin)
39 hashnncl 14405 . . . . . . . . . 10 (𝐾 ∈ Fin → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4038, 39syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝐾) ∈ ℕ ↔ 𝐾 ≠ ∅))
4135, 40mpbird 257 . . . . . . . 8 (𝜑 → (♯‘𝐾) ∈ ℕ)
4241nnzd 12640 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℤ)
43 hashcl 14395 . . . . . . . . 9 (𝑁 ∈ Fin → (♯‘𝑁) ∈ ℕ0)
4425, 43syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑁) ∈ ℕ0)
4544nn0zd 12639 . . . . . . 7 (𝜑 → (♯‘𝑁) ∈ ℤ)
46 pwfi 9357 . . . . . . . . . . 11 (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin)
473, 46sylib 218 . . . . . . . . . 10 (𝜑 → 𝒫 𝑋 ∈ Fin)
48 eqid 2737 . . . . . . . . . . . . 13 (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁)
491, 48eqger 19196 . . . . . . . . . . . 12 (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er 𝑋)
5020, 49syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺 ~QG 𝑁) Er 𝑋)
5150qsss 8818 . . . . . . . . . 10 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ⊆ 𝒫 𝑋)
5247, 51ssfid 9301 . . . . . . . . 9 (𝜑 → (𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin)
53 hashcl 14395 . . . . . . . . 9 ((𝑋 / (𝐺 ~QG 𝑁)) ∈ Fin → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5452, 53syl 17 . . . . . . . 8 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℕ0)
5554nn0zd 12639 . . . . . . 7 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ)
56 dvdscmul 16320 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝑁) ∈ ℤ ∧ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5742, 45, 55, 56syl3anc 1373 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑁) → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁))))
5831, 57mpd 15 . . . . 5 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
59 hashcl 14395 . . . . . . . . 9 (𝑋 ∈ Fin → (♯‘𝑋) ∈ ℕ0)
603, 59syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑋) ∈ ℕ0)
6160nn0cnd 12589 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℂ)
6241nncnd 12282 . . . . . . 7 (𝜑 → (♯‘𝐾) ∈ ℂ)
6341nnne0d 12316 . . . . . . 7 (𝜑 → (♯‘𝐾) ≠ 0)
6461, 62, 63divcan1d 12044 . . . . . 6 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = (♯‘𝑋))
651, 48, 20, 3lagsubg2 19212 . . . . . 6 (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6664, 65eqtrd 2777 . . . . 5 (𝜑 → (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) = ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝑁)))
6758, 66breqtrrd 5171 . . . 4 (𝜑 → ((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)))
681lagsubg 19213 . . . . . . 7 ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝐾) ∥ (♯‘𝑋))
6913, 3, 68syl2anc 584 . . . . . 6 (𝜑 → (♯‘𝐾) ∥ (♯‘𝑋))
7060nn0zd 12639 . . . . . . 7 (𝜑 → (♯‘𝑋) ∈ ℤ)
71 dvdsval2 16293 . . . . . . 7 (((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7242, 63, 70, 71syl3anc 1373 . . . . . 6 (𝜑 → ((♯‘𝐾) ∥ (♯‘𝑋) ↔ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ))
7369, 72mpbid 232 . . . . 5 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ)
74 dvdsmulcr 16323 . . . . 5 (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∈ ℤ ∧ ((♯‘𝑋) / (♯‘𝐾)) ∈ ℤ ∧ ((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0)) → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7555, 73, 42, 63, 74syl112anc 1376 . . . 4 (𝜑 → (((♯‘(𝑋 / (𝐺 ~QG 𝑁))) · (♯‘𝐾)) ∥ (((♯‘𝑋) / (♯‘𝐾)) · (♯‘𝐾)) ↔ (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾))))
7667, 75mpbid 232 . . 3 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (♯‘𝐾)))
771, 3, 8slwhash 19642 . . . 4 (𝜑 → (♯‘𝐾) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
7877oveq2d 7447 . . 3 (𝜑 → ((♯‘𝑋) / (♯‘𝐾)) = ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
7976, 78breqtrd 5169 . 2 (𝜑 → (♯‘(𝑋 / (𝐺 ~QG 𝑁))) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
8011, 79eqbrtrd 5165 1 (𝜑 → (♯‘(𝑃 pSyl 𝐺)) ∥ ((♯‘𝑋) / (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  wne 2940  wral 3061  {crab 3436  wss 3951  c0 4333  𝒫 cpw 4600   class class class wbr 5143  cmpt 5225  ran crn 5686  cfv 6561  (class class class)co 7431  cmpo 7433   Er wer 8742   / cqs 8744  Fincfn 8985  0cc0 11155   · cmul 11160   / 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  -gcsg 18953  SubGrpcsubg 19138  NrmSGrpcnsg 19139   ~QG cqg 19140   pSyl cslw 19545
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-nsg 19142  df-eqg 19143  df-ghm 19231  df-ga 19308  df-od 19546  df-pgp 19548  df-slw 19549
This theorem is referenced by:  sylow3  19651
  Copyright terms: Public domain W3C validator