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

Theorem sylow1lem4 18217
Description: Lemma for sylow1 18219. The stabilizer subgroup of any element of 𝑆 is at most 𝑃𝑁 in size. (Contributed by Mario Carneiro, 15-Jan-2015.)
Hypotheses
Ref Expression
sylow1.x 𝑋 = (Base‘𝐺)
sylow1.g (𝜑𝐺 ∈ Grp)
sylow1.f (𝜑𝑋 ∈ Fin)
sylow1.p (𝜑𝑃 ∈ ℙ)
sylow1.n (𝜑𝑁 ∈ ℕ0)
sylow1.d (𝜑 → (𝑃𝑁) ∥ (♯‘𝑋))
sylow1lem.a + = (+g𝐺)
sylow1lem.s 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}
sylow1lem.m = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
sylow1lem3.1 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔𝑋 (𝑔 𝑥) = 𝑦)}
sylow1lem4.b (𝜑𝐵𝑆)
sylow1lem4.h 𝐻 = {𝑢𝑋 ∣ (𝑢 𝐵) = 𝐵}
Assertion
Ref Expression
sylow1lem4 (𝜑 → (♯‘𝐻) ≤ (𝑃𝑁))
Distinct variable groups:   𝑔,𝑠,𝑢,𝑥,𝑦,𝑧,𝐵   𝑔,𝐻,𝑥,𝑦   𝑆,𝑔,𝑢,𝑥,𝑦,𝑧   𝑔,𝑁,𝑠,𝑢,𝑥,𝑦,𝑧   𝑔,𝑋,𝑠,𝑢,𝑥,𝑦,𝑧   + ,𝑠,𝑢,𝑥,𝑦,𝑧   𝑧,   ,𝑔,𝑢,𝑥,𝑦,𝑧   𝑔,𝐺,𝑠,𝑢,𝑥,𝑦,𝑧   𝑃,𝑔,𝑠,𝑢,𝑥,𝑦,𝑧   𝜑,𝑢,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑔,𝑠)   + (𝑔)   (𝑠)   (𝑥,𝑦,𝑢,𝑔,𝑠)   𝑆(𝑠)   𝐻(𝑧,𝑢,𝑠)

Proof of Theorem sylow1lem4
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow1lem4.b . . . . . . . . . 10 (𝜑𝐵𝑆)
2 fveqeq2 6417 . . . . . . . . . . 11 (𝑠 = 𝐵 → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘𝐵) = (𝑃𝑁)))
3 sylow1lem.s . . . . . . . . . . 11 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}
42, 3elrab2 3562 . . . . . . . . . 10 (𝐵𝑆 ↔ (𝐵 ∈ 𝒫 𝑋 ∧ (♯‘𝐵) = (𝑃𝑁)))
51, 4sylib 209 . . . . . . . . 9 (𝜑 → (𝐵 ∈ 𝒫 𝑋 ∧ (♯‘𝐵) = (𝑃𝑁)))
65simprd 485 . . . . . . . 8 (𝜑 → (♯‘𝐵) = (𝑃𝑁))
7 sylow1.p . . . . . . . . . 10 (𝜑𝑃 ∈ ℙ)
8 prmnn 15606 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
97, 8syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ)
10 sylow1.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
119, 10nnexpcld 13253 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ ℕ)
126, 11eqeltrd 2885 . . . . . . 7 (𝜑 → (♯‘𝐵) ∈ ℕ)
1312nnne0d 11351 . . . . . 6 (𝜑 → (♯‘𝐵) ≠ 0)
14 hasheq0 13372 . . . . . . . 8 (𝐵𝑆 → ((♯‘𝐵) = 0 ↔ 𝐵 = ∅))
1514necon3bid 3022 . . . . . . 7 (𝐵𝑆 → ((♯‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅))
161, 15syl 17 . . . . . 6 (𝜑 → ((♯‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅))
1713, 16mpbid 223 . . . . 5 (𝜑𝐵 ≠ ∅)
18 n0 4132 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑎 𝑎𝐵)
1917, 18sylib 209 . . . 4 (𝜑 → ∃𝑎 𝑎𝐵)
201adantr 468 . . . . 5 ((𝜑𝑎𝐵) → 𝐵𝑆)
21 simplr 776 . . . . . . . . . . 11 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑎𝐵)
22 oveq2 6882 . . . . . . . . . . . 12 (𝑧 = 𝑎 → (𝑏 + 𝑧) = (𝑏 + 𝑎))
23 eqid 2806 . . . . . . . . . . . 12 (𝑧𝐵 ↦ (𝑏 + 𝑧)) = (𝑧𝐵 ↦ (𝑏 + 𝑧))
24 ovex 6906 . . . . . . . . . . . 12 (𝑏 + 𝑎) ∈ V
2522, 23, 24fvmpt 6503 . . . . . . . . . . 11 (𝑎𝐵 → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎))
2621, 25syl 17 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎))
27 ovex 6906 . . . . . . . . . . . 12 (𝑏 + 𝑧) ∈ V
2827, 23fnmpti 6233 . . . . . . . . . . 11 (𝑧𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵
29 fnfvelrn 6578 . . . . . . . . . . 11 (((𝑧𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵𝑎𝐵) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
3028, 21, 29sylancr 577 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
3126, 30eqeltrrd 2886 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
32 sylow1lem4.h . . . . . . . . . . . 12 𝐻 = {𝑢𝑋 ∣ (𝑢 𝐵) = 𝐵}
33 ssrab2 3884 . . . . . . . . . . . 12 {𝑢𝑋 ∣ (𝑢 𝐵) = 𝐵} ⊆ 𝑋
3432, 33eqsstri 3832 . . . . . . . . . . 11 𝐻𝑋
35 simpr 473 . . . . . . . . . . 11 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑏𝐻)
3634, 35sseldi 3796 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑏𝑋)
371ad2antrr 708 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝐵𝑆)
38 mptexg 6709 . . . . . . . . . . 11 (𝐵𝑆 → (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
39 rnexg 7328 . . . . . . . . . . 11 ((𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V → ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
4037, 38, 393syl 18 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
41 simpr 473 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = 𝐵) → 𝑦 = 𝐵)
42 simpl 470 . . . . . . . . . . . . . 14 ((𝑥 = 𝑏𝑦 = 𝐵) → 𝑥 = 𝑏)
4342oveq1d 6889 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = 𝐵) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
4441, 43mpteq12dv 4927 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = 𝐵) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4544rneqd 5554 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = 𝐵) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
46 sylow1lem.m . . . . . . . . . . 11 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
4745, 46ovmpt2ga 7020 . . . . . . . . . 10 ((𝑏𝑋𝐵𝑆 ∧ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V) → (𝑏 𝐵) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4836, 37, 40, 47syl3anc 1483 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 𝐵) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4931, 48eleqtrrd 2888 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ (𝑏 𝐵))
50 oveq1 6881 . . . . . . . . . . . 12 (𝑢 = 𝑏 → (𝑢 𝐵) = (𝑏 𝐵))
5150eqeq1d 2808 . . . . . . . . . . 11 (𝑢 = 𝑏 → ((𝑢 𝐵) = 𝐵 ↔ (𝑏 𝐵) = 𝐵))
5251, 32elrab2 3562 . . . . . . . . . 10 (𝑏𝐻 ↔ (𝑏𝑋 ∧ (𝑏 𝐵) = 𝐵))
5352simprbi 486 . . . . . . . . 9 (𝑏𝐻 → (𝑏 𝐵) = 𝐵)
5453adantl 469 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 𝐵) = 𝐵)
5549, 54eleqtrd 2887 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ 𝐵)
5655ex 399 . . . . . 6 ((𝜑𝑎𝐵) → (𝑏𝐻 → (𝑏 + 𝑎) ∈ 𝐵))
57 sylow1.g . . . . . . . . 9 (𝜑𝐺 ∈ Grp)
5857ad2antrr 708 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝐺 ∈ Grp)
59 simprl 778 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑏𝐻)
6034, 59sseldi 3796 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑏𝑋)
61 simprr 780 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑐𝐻)
6234, 61sseldi 3796 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑐𝑋)
635simpld 484 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝑋)
6463elpwid 4363 . . . . . . . . . 10 (𝜑𝐵𝑋)
6564sselda 3798 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝑎𝑋)
6665adantr 468 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑎𝑋)
67 sylow1.x . . . . . . . . 9 𝑋 = (Base‘𝐺)
68 sylow1lem.a . . . . . . . . 9 + = (+g𝐺)
6967, 68grprcan 17660 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑎𝑋)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐))
7058, 60, 62, 66, 69syl13anc 1484 . . . . . . 7 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐))
7170ex 399 . . . . . 6 ((𝜑𝑎𝐵) → ((𝑏𝐻𝑐𝐻) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐)))
7256, 71dom2d 8233 . . . . 5 ((𝜑𝑎𝐵) → (𝐵𝑆𝐻𝐵))
7320, 72mpd 15 . . . 4 ((𝜑𝑎𝐵) → 𝐻𝐵)
7419, 73exlimddv 2026 . . 3 (𝜑𝐻𝐵)
75 sylow1.f . . . . 5 (𝜑𝑋 ∈ Fin)
76 ssfi 8419 . . . . 5 ((𝑋 ∈ Fin ∧ 𝐻𝑋) → 𝐻 ∈ Fin)
7775, 34, 76sylancl 576 . . . 4 (𝜑𝐻 ∈ Fin)
78 ssfi 8419 . . . . 5 ((𝑋 ∈ Fin ∧ 𝐵𝑋) → 𝐵 ∈ Fin)
7975, 64, 78syl2anc 575 . . . 4 (𝜑𝐵 ∈ Fin)
80 hashdom 13386 . . . 4 ((𝐻 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐻) ≤ (♯‘𝐵) ↔ 𝐻𝐵))
8177, 79, 80syl2anc 575 . . 3 (𝜑 → ((♯‘𝐻) ≤ (♯‘𝐵) ↔ 𝐻𝐵))
8274, 81mpbird 248 . 2 (𝜑 → (♯‘𝐻) ≤ (♯‘𝐵))
8382, 6breqtrd 4870 1 (𝜑 → (♯‘𝐻) ≤ (𝑃𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2156  wne 2978  wrex 3097  {crab 3100  Vcvv 3391  wss 3769  c0 4116  𝒫 cpw 4351  {cpr 4372   class class class wbr 4844  {copab 4906  cmpt 4923  ran crn 5312   Fn wfn 6096  cfv 6101  (class class class)co 6874  cmpt2 6876  cdom 8190  Fincfn 8192  0cc0 10221  cle 10360  cn 11305  0cn0 11559  cexp 13083  chash 13337  cdvds 15203  cprime 15603  Basecbs 16068  +gcplusg 16153  Grpcgrp 17627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-oadd 7800  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-card 9048  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-n0 11560  df-xnn0 11630  df-z 11644  df-uz 11905  df-fz 12550  df-seq 13025  df-exp 13084  df-hash 13338  df-prm 15604  df-0g 16307  df-mgm 17447  df-sgrp 17489  df-mnd 17500  df-grp 17630
This theorem is referenced by:  sylow1lem5  18218
  Copyright terms: Public domain W3C validator