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

Theorem sylow1lem4 18717
 Description: Lemma for sylow1 18719. 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 6661 . . . . . . . . . . 11 (𝑠 = 𝐵 → ((♯‘𝑠) = (𝑃𝑁) ↔ (♯‘𝐵) = (𝑃𝑁)))
3 sylow1lem.s . . . . . . . . . . 11 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃𝑁)}
42, 3elrab2 3658 . . . . . . . . . 10 (𝐵𝑆 ↔ (𝐵 ∈ 𝒫 𝑋 ∧ (♯‘𝐵) = (𝑃𝑁)))
51, 4sylib 221 . . . . . . . . 9 (𝜑 → (𝐵 ∈ 𝒫 𝑋 ∧ (♯‘𝐵) = (𝑃𝑁)))
65simprd 499 . . . . . . . 8 (𝜑 → (♯‘𝐵) = (𝑃𝑁))
7 sylow1.p . . . . . . . . . 10 (𝜑𝑃 ∈ ℙ)
8 prmnn 16007 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
97, 8syl 17 . . . . . . . . 9 (𝜑𝑃 ∈ ℕ)
10 sylow1.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ0)
119, 10nnexpcld 13602 . . . . . . . 8 (𝜑 → (𝑃𝑁) ∈ ℕ)
126, 11eqeltrd 2914 . . . . . . 7 (𝜑 → (♯‘𝐵) ∈ ℕ)
1312nnne0d 11675 . . . . . 6 (𝜑 → (♯‘𝐵) ≠ 0)
14 hasheq0 13720 . . . . . . . 8 (𝐵𝑆 → ((♯‘𝐵) = 0 ↔ 𝐵 = ∅))
1514necon3bid 3055 . . . . . . 7 (𝐵𝑆 → ((♯‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅))
161, 15syl 17 . . . . . 6 (𝜑 → ((♯‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅))
1713, 16mpbid 235 . . . . 5 (𝜑𝐵 ≠ ∅)
18 n0 4282 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑎 𝑎𝐵)
1917, 18sylib 221 . . . 4 (𝜑 → ∃𝑎 𝑎𝐵)
201adantr 484 . . . . 5 ((𝜑𝑎𝐵) → 𝐵𝑆)
21 simplr 768 . . . . . . . . . . 11 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑎𝐵)
22 oveq2 7148 . . . . . . . . . . . 12 (𝑧 = 𝑎 → (𝑏 + 𝑧) = (𝑏 + 𝑎))
23 eqid 2822 . . . . . . . . . . . 12 (𝑧𝐵 ↦ (𝑏 + 𝑧)) = (𝑧𝐵 ↦ (𝑏 + 𝑧))
24 ovex 7173 . . . . . . . . . . . 12 (𝑏 + 𝑎) ∈ V
2522, 23, 24fvmpt 6750 . . . . . . . . . . 11 (𝑎𝐵 → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎))
2621, 25syl 17 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎))
27 ovex 7173 . . . . . . . . . . . 12 (𝑏 + 𝑧) ∈ V
2827, 23fnmpti 6471 . . . . . . . . . . 11 (𝑧𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵
29 fnfvelrn 6830 . . . . . . . . . . 11 (((𝑧𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵𝑎𝐵) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
3028, 21, 29sylancr 590 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ((𝑧𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
3126, 30eqeltrrd 2915 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
32 sylow1lem4.h . . . . . . . . . . . 12 𝐻 = {𝑢𝑋 ∣ (𝑢 𝐵) = 𝐵}
3332ssrab3 4032 . . . . . . . . . . 11 𝐻𝑋
34 simpr 488 . . . . . . . . . . 11 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑏𝐻)
3533, 34sseldi 3940 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝑏𝑋)
361ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → 𝐵𝑆)
37 mptexg 6966 . . . . . . . . . . 11 (𝐵𝑆 → (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
38 rnexg 7600 . . . . . . . . . . 11 ((𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V → ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
3936, 37, 383syl 18 . . . . . . . . . 10 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V)
40 simpr 488 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = 𝐵) → 𝑦 = 𝐵)
41 simpl 486 . . . . . . . . . . . . . 14 ((𝑥 = 𝑏𝑦 = 𝐵) → 𝑥 = 𝑏)
4241oveq1d 7155 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = 𝐵) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
4340, 42mpteq12dv 5127 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = 𝐵) → (𝑧𝑦 ↦ (𝑥 + 𝑧)) = (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4443rneqd 5785 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = 𝐵) → ran (𝑧𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
45 sylow1lem.m . . . . . . . . . . 11 = (𝑥𝑋, 𝑦𝑆 ↦ ran (𝑧𝑦 ↦ (𝑥 + 𝑧)))
4644, 45ovmpoga 7288 . . . . . . . . . 10 ((𝑏𝑋𝐵𝑆 ∧ ran (𝑧𝐵 ↦ (𝑏 + 𝑧)) ∈ V) → (𝑏 𝐵) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4735, 36, 39, 46syl3anc 1368 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 𝐵) = ran (𝑧𝐵 ↦ (𝑏 + 𝑧)))
4831, 47eleqtrrd 2917 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ (𝑏 𝐵))
49 oveq1 7147 . . . . . . . . . . . 12 (𝑢 = 𝑏 → (𝑢 𝐵) = (𝑏 𝐵))
5049eqeq1d 2824 . . . . . . . . . . 11 (𝑢 = 𝑏 → ((𝑢 𝐵) = 𝐵 ↔ (𝑏 𝐵) = 𝐵))
5150, 32elrab2 3658 . . . . . . . . . 10 (𝑏𝐻 ↔ (𝑏𝑋 ∧ (𝑏 𝐵) = 𝐵))
5251simprbi 500 . . . . . . . . 9 (𝑏𝐻 → (𝑏 𝐵) = 𝐵)
5352adantl 485 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 𝐵) = 𝐵)
5448, 53eleqtrd 2916 . . . . . . 7 (((𝜑𝑎𝐵) ∧ 𝑏𝐻) → (𝑏 + 𝑎) ∈ 𝐵)
5554ex 416 . . . . . 6 ((𝜑𝑎𝐵) → (𝑏𝐻 → (𝑏 + 𝑎) ∈ 𝐵))
56 sylow1.g . . . . . . . . 9 (𝜑𝐺 ∈ Grp)
5756ad2antrr 725 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝐺 ∈ Grp)
58 simprl 770 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑏𝐻)
5933, 58sseldi 3940 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑏𝑋)
60 simprr 772 . . . . . . . . 9 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑐𝐻)
6133, 60sseldi 3940 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑐𝑋)
625simpld 498 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝑋)
6362elpwid 4522 . . . . . . . . . 10 (𝜑𝐵𝑋)
6463sselda 3942 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝑎𝑋)
6564adantr 484 . . . . . . . 8 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → 𝑎𝑋)
66 sylow1.x . . . . . . . . 9 𝑋 = (Base‘𝐺)
67 sylow1lem.a . . . . . . . . 9 + = (+g𝐺)
6866, 67grprcan 18128 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑎𝑋)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐))
6957, 59, 61, 65, 68syl13anc 1369 . . . . . . 7 (((𝜑𝑎𝐵) ∧ (𝑏𝐻𝑐𝐻)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐))
7069ex 416 . . . . . 6 ((𝜑𝑎𝐵) → ((𝑏𝐻𝑐𝐻) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐)))
7155, 70dom2d 8537 . . . . 5 ((𝜑𝑎𝐵) → (𝐵𝑆𝐻𝐵))
7220, 71mpd 15 . . . 4 ((𝜑𝑎𝐵) → 𝐻𝐵)
7319, 72exlimddv 1936 . . 3 (𝜑𝐻𝐵)
74 sylow1.f . . . . 5 (𝜑𝑋 ∈ Fin)
75 ssfi 8726 . . . . 5 ((𝑋 ∈ Fin ∧ 𝐻𝑋) → 𝐻 ∈ Fin)
7674, 33, 75sylancl 589 . . . 4 (𝜑𝐻 ∈ Fin)
7774, 63ssfid 8729 . . . 4 (𝜑𝐵 ∈ Fin)
78 hashdom 13736 . . . 4 ((𝐻 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐻) ≤ (♯‘𝐵) ↔ 𝐻𝐵))
7976, 77, 78syl2anc 587 . . 3 (𝜑 → ((♯‘𝐻) ≤ (♯‘𝐵) ↔ 𝐻𝐵))
8073, 79mpbird 260 . 2 (𝜑 → (♯‘𝐻) ≤ (♯‘𝐵))
8180, 6breqtrd 5068 1 (𝜑 → (♯‘𝐻) ≤ (𝑃𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2114   ≠ wne 3011  ∃wrex 3131  {crab 3134  Vcvv 3469   ⊆ wss 3908  ∅c0 4265  𝒫 cpw 4511  {cpr 4541   class class class wbr 5042  {copab 5104   ↦ cmpt 5122  ran crn 5533   Fn wfn 6329  ‘cfv 6334  (class class class)co 7140   ∈ cmpo 7142   ≼ cdom 8494  Fincfn 8496  0cc0 10526   ≤ cle 10665  ℕcn 11625  ℕ0cn0 11885  ↑cexp 13425  ♯chash 13686   ∥ cdvds 15598  ℙcprime 16004  Basecbs 16474  +gcplusg 16556  Grpcgrp 18094 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12886  df-seq 13365  df-exp 13426  df-hash 13687  df-prm 16005  df-0g 16706  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-grp 18097 This theorem is referenced by:  sylow1lem5  18718
 Copyright terms: Public domain W3C validator