# Metamath Proof Explorer

## Theorem lagsubg2

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
Hypotheses lagsubg.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
lagsubg.2
lagsubg.3 ${⊢}{\phi }\to {Y}\in \mathrm{SubGrp}\left({G}\right)$
lagsubg.4 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
Assertion lagsubg2

### Proof

Step Hyp Ref Expression
1 lagsubg.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 lagsubg.2
3 lagsubg.3 ${⊢}{\phi }\to {Y}\in \mathrm{SubGrp}\left({G}\right)$
4 lagsubg.4 ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
5 1 2 eqger
6 3 5 syl
7 6 4 qshash
8 1 2 eqgen
9 3 8 sylan
10 1 subgss ${⊢}{Y}\in \mathrm{SubGrp}\left({G}\right)\to {Y}\subseteq {X}$
11 3 10 syl ${⊢}{\phi }\to {Y}\subseteq {X}$
12 4 11 ssfid ${⊢}{\phi }\to {Y}\in \mathrm{Fin}$
15 6 qsss
16 15 sselda
17 16 elpwid
18 14 17 ssfid
19 hashen ${⊢}\left({Y}\in \mathrm{Fin}\wedge {x}\in \mathrm{Fin}\right)\to \left(\left|{Y}\right|=\left|{x}\right|↔{Y}\approx {x}\right)$
20 13 18 19 syl2anc
21 9 20 mpbird
22 21 sumeq2dv
23 pwfi ${⊢}{X}\in \mathrm{Fin}↔𝒫{X}\in \mathrm{Fin}$
24 4 23 sylib ${⊢}{\phi }\to 𝒫{X}\in \mathrm{Fin}$
25 24 15 ssfid
26 hashcl ${⊢}{Y}\in \mathrm{Fin}\to \left|{Y}\right|\in {ℕ}_{0}$
27 12 26 syl ${⊢}{\phi }\to \left|{Y}\right|\in {ℕ}_{0}$
28 27 nn0cnd ${⊢}{\phi }\to \left|{Y}\right|\in ℂ$
29 fsumconst
30 25 28 29 syl2anc
31 7 22 30 3eqtr2d