Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > orbsta2 | Structured version Visualization version GIF version |
Description: Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Ref | Expression |
---|---|
orbsta2.x | ⊢ 𝑋 = (Base‘𝐺) |
orbsta2.h | ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} |
orbsta2.r | ⊢ ∼ = (𝐺 ~QG 𝐻) |
orbsta2.o | ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
Ref | Expression |
---|---|
orbsta2 | ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐴]𝑂) · (♯‘𝐻))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbsta2.x | . . 3 ⊢ 𝑋 = (Base‘𝐺) | |
2 | orbsta2.r | . . 3 ⊢ ∼ = (𝐺 ~QG 𝐻) | |
3 | orbsta2.h | . . . . 5 ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴} | |
4 | 1, 3 | gastacl 18736 | . . . 4 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺)) |
5 | 4 | adantr 484 | . . 3 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → 𝐻 ∈ (SubGrp‘𝐺)) |
6 | simpr 488 | . . 3 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → 𝑋 ∈ Fin) | |
7 | 1, 2, 5, 6 | lagsubg2 18638 | . 2 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝐻))) |
8 | pwfi 8882 | . . . . . 6 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin) | |
9 | 6, 8 | sylib 221 | . . . . 5 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → 𝒫 𝑋 ∈ Fin) |
10 | 1, 2 | eqger 18627 | . . . . . . 7 ⊢ (𝐻 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
11 | 5, 10 | syl 17 | . . . . . 6 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → ∼ Er 𝑋) |
12 | 11 | qsss 8484 | . . . . 5 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (𝑋 / ∼ ) ⊆ 𝒫 𝑋) |
13 | 9, 12 | ssfid 8928 | . . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (𝑋 / ∼ ) ∈ Fin) |
14 | eqid 2739 | . . . . . 6 ⊢ ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) = ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉) | |
15 | orbsta2.o | . . . . . 6 ⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} | |
16 | 1, 3, 2, 14, 15 | orbsta 18740 | . . . . 5 ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉):(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂) |
17 | 16 | adantr 484 | . . . 4 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → ran (𝑘 ∈ 𝑋 ↦ 〈[𝑘] ∼ , (𝑘 ⊕ 𝐴)〉):(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂) |
18 | 13, 17 | hasheqf1od 13953 | . . 3 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘(𝑋 / ∼ )) = (♯‘[𝐴]𝑂)) |
19 | 18 | oveq1d 7250 | . 2 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → ((♯‘(𝑋 / ∼ )) · (♯‘𝐻)) = ((♯‘[𝐴]𝑂) · (♯‘𝐻))) |
20 | 7, 19 | eqtrd 2779 | 1 ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐴]𝑂) · (♯‘𝐻))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2112 ∃wrex 3065 {crab 3068 ⊆ wss 3883 𝒫 cpw 4530 {cpr 4560 〈cop 4564 {copab 5132 ↦ cmpt 5152 ran crn 5570 –1-1-onto→wf1o 6400 ‘cfv 6401 (class class class)co 7235 Er wer 8412 [cec 8413 / cqs 8414 Fincfn 8650 · cmul 10764 ♯chash 13929 Basecbs 16793 SubGrpcsubg 18570 ~QG cqg 18572 GrpAct cga 18716 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5196 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-inf2 9286 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 ax-pre-sup 10837 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-se 5528 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-isom 6410 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-om 7667 df-1st 7783 df-2nd 7784 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-1o 8226 df-er 8415 df-ec 8417 df-qs 8421 df-map 8534 df-en 8651 df-dom 8652 df-sdom 8653 df-fin 8654 df-sup 9088 df-oi 9156 df-card 9585 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-div 11520 df-nn 11861 df-2 11923 df-3 11924 df-n0 12121 df-z 12207 df-uz 12469 df-rp 12617 df-fz 13126 df-fzo 13269 df-seq 13607 df-exp 13668 df-hash 13930 df-cj 14695 df-re 14696 df-im 14697 df-sqrt 14831 df-abs 14832 df-clim 15082 df-sum 15283 df-sets 16750 df-slot 16768 df-ndx 16778 df-base 16794 df-ress 16818 df-plusg 16848 df-0g 16979 df-mgm 18147 df-sgrp 18196 df-mnd 18207 df-grp 18401 df-minusg 18402 df-subg 18573 df-eqg 18575 df-ga 18717 |
This theorem is referenced by: sylow1lem5 19024 sylow2alem2 19040 sylow3lem3 19051 |
Copyright terms: Public domain | W3C validator |