| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > lagsubg2 | Structured version Visualization version GIF version | ||
| Description: Lagrange's theorem for finite groups. Call the "order" of a group the cardinal number of the basic set of the group, and "index of a subgroup" the cardinal number of the set of left (or right, this is the same) cosets of this subgroup. Then the order of the group is the (cardinal) product of the order of any of its subgroups by the index of this subgroup. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| Ref | Expression |
|---|---|
| lagsubg.1 | ⊢ 𝑋 = (Base‘𝐺) |
| lagsubg.2 | ⊢ ∼ = (𝐺 ~QG 𝑌) |
| lagsubg.3 | ⊢ (𝜑 → 𝑌 ∈ (SubGrp‘𝐺)) |
| lagsubg.4 | ⊢ (𝜑 → 𝑋 ∈ Fin) |
| Ref | Expression |
|---|---|
| lagsubg2 | ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lagsubg.3 | . . . 4 ⊢ (𝜑 → 𝑌 ∈ (SubGrp‘𝐺)) | |
| 2 | lagsubg.1 | . . . . 5 ⊢ 𝑋 = (Base‘𝐺) | |
| 3 | lagsubg.2 | . . . . 5 ⊢ ∼ = (𝐺 ~QG 𝑌) | |
| 4 | 2, 3 | eqger 19220 | . . . 4 ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
| 5 | 1, 4 | syl 17 | . . 3 ⊢ (𝜑 → ∼ Er 𝑋) |
| 6 | lagsubg.4 | . . 3 ⊢ (𝜑 → 𝑋 ∈ Fin) | |
| 7 | 5, 6 | qshash 15856 | . 2 ⊢ (𝜑 → (♯‘𝑋) = Σ𝑥 ∈ (𝑋 / ∼ )(♯‘𝑥)) |
| 8 | 2, 3 | eqgen 19223 | . . . . 5 ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝑥) |
| 9 | 1, 8 | sylan 589 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝑥) |
| 10 | 2 | subgss 19170 | . . . . . . . 8 ⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
| 11 | 1, 10 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
| 12 | 6, 11 | ssfid 9214 | . . . . . 6 ⊢ (𝜑 → 𝑌 ∈ Fin) |
| 13 | 12 | adantr 484 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑌 ∈ Fin) |
| 14 | 6 | adantr 484 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑋 ∈ Fin) |
| 15 | 5 | qsss 8758 | . . . . . . . 8 ⊢ (𝜑 → (𝑋 / ∼ ) ⊆ 𝒫 𝑋) |
| 16 | 15 | sselda 3937 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑥 ∈ 𝒫 𝑋) |
| 17 | 16 | elpwid 4565 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑥 ⊆ 𝑋) |
| 18 | 14, 17 | ssfid 9214 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → 𝑥 ∈ Fin) |
| 19 | hashen 14361 | . . . . 5 ⊢ ((𝑌 ∈ Fin ∧ 𝑥 ∈ Fin) → ((♯‘𝑌) = (♯‘𝑥) ↔ 𝑌 ≈ 𝑥)) | |
| 20 | 13, 18, 19 | syl2anc 593 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → ((♯‘𝑌) = (♯‘𝑥) ↔ 𝑌 ≈ 𝑥)) |
| 21 | 9, 20 | mpbird 259 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 / ∼ )) → (♯‘𝑌) = (♯‘𝑥)) |
| 22 | 21 | sumeq2dv 15730 | . 2 ⊢ (𝜑 → Σ𝑥 ∈ (𝑋 / ∼ )(♯‘𝑌) = Σ𝑥 ∈ (𝑋 / ∼ )(♯‘𝑥)) |
| 23 | pwfi 9264 | . . . . 5 ⊢ (𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin) | |
| 24 | 6, 23 | sylib 220 | . . . 4 ⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
| 25 | 24, 15 | ssfid 9214 | . . 3 ⊢ (𝜑 → (𝑋 / ∼ ) ∈ Fin) |
| 26 | hashcl 14370 | . . . . 5 ⊢ (𝑌 ∈ Fin → (♯‘𝑌) ∈ ℕ0) | |
| 27 | 12, 26 | syl 17 | . . . 4 ⊢ (𝜑 → (♯‘𝑌) ∈ ℕ0) |
| 28 | 27 | nn0cnd 12545 | . . 3 ⊢ (𝜑 → (♯‘𝑌) ∈ ℂ) |
| 29 | fsumconst 15818 | . . 3 ⊢ (((𝑋 / ∼ ) ∈ Fin ∧ (♯‘𝑌) ∈ ℂ) → Σ𝑥 ∈ (𝑋 / ∼ )(♯‘𝑌) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) | |
| 30 | 25, 28, 29 | syl2anc 593 | . 2 ⊢ (𝜑 → Σ𝑥 ∈ (𝑋 / ∼ )(♯‘𝑌) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) |
| 31 | 7, 22, 30 | 3eqtr2d 2804 | 1 ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1561 ∈ wcel 2143 ⊆ wss 3905 𝒫 cpw 4556 class class class wbr 5101 ‘cfv 6522 (class class class)co 7397 Er wer 8676 / cqs 8678 ≈ cen 8925 Fincfn 8928 ℂcc 11072 · cmul 11079 ℕ0cn0 12482 ♯chash 14344 Σcsu 15714 Basecbs 17246 SubGrpcsubg 19163 ~QG cqg 19165 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5228 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719 ax-inf2 9597 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-pre-sup 11152 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-disj 5069 df-br 5102 df-opab 5164 df-mpt 5183 df-tr 5209 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-se 5602 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6289 df-ord 6350 df-on 6351 df-lim 6352 df-suc 6353 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-isom 6531 df-riota 7354 df-ov 7400 df-oprab 7401 df-mpo 7402 df-om 7848 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8382 df-1o 8438 df-er 8679 df-ec 8681 df-qs 8685 df-en 8929 df-dom 8930 df-sdom 8931 df-fin 8932 df-sup 9389 df-oi 9459 df-card 9898 df-pnf 11219 df-mnf 11220 df-xr 11221 df-ltxr 11222 df-le 11223 df-sub 11417 df-neg 11418 df-div 11846 df-nn 12212 df-2 12281 df-3 12282 df-n0 12483 df-z 12570 df-uz 12841 df-rp 12995 df-fz 13514 df-fzo 13661 df-seq 14016 df-exp 14076 df-hash 14345 df-cj 15127 df-re 15128 df-im 15129 df-sqrt 15263 df-abs 15264 df-clim 15516 df-sum 15715 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17247 df-ress 17268 df-plusg 17300 df-0g 17471 df-mgm 18675 df-sgrp 18754 df-mnd 18770 df-grp 18979 df-minusg 18980 df-subg 19166 df-eqg 19168 |
| This theorem is referenced by: lagsubg 19237 orbsta2 19355 sylow2blem3 19663 sylow3lem3 19670 sylow3lem4 19671 |
| Copyright terms: Public domain | W3C validator |