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 = ( Base ` G )
lagsubg.2
|- .~ = ( G ~QG Y )
lagsubg.3
|- ( ph -> Y e. ( SubGrp ` G ) )
lagsubg.4
|- ( ph -> X e. Fin )
Assertion lagsubg2
|- ( ph -> ( # ` X ) = ( ( # ` ( X /. .~ ) ) x. ( # ` Y ) ) )

Proof

Step Hyp Ref Expression
1 lagsubg.1
 |-  X = ( Base ` G )
2 lagsubg.2
 |-  .~ = ( G ~QG Y )
3 lagsubg.3
 |-  ( ph -> Y e. ( SubGrp ` G ) )
4 lagsubg.4
 |-  ( ph -> X e. Fin )
5 1 2 eqger
 |-  ( Y e. ( SubGrp ` G ) -> .~ Er X )
6 3 5 syl
 |-  ( ph -> .~ Er X )
7 6 4 qshash
 |-  ( ph -> ( # ` X ) = sum_ x e. ( X /. .~ ) ( # ` x ) )
8 1 2 eqgen
 |-  ( ( Y e. ( SubGrp ` G ) /\ x e. ( X /. .~ ) ) -> Y ~~ x )
9 3 8 sylan
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> Y ~~ x )
10 1 subgss
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
11 3 10 syl
 |-  ( ph -> Y C_ X )
12 4 11 ssfid
 |-  ( ph -> Y e. Fin )
13 12 adantr
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> Y e. Fin )
14 4 adantr
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> X e. Fin )
15 6 qsss
 |-  ( ph -> ( X /. .~ ) C_ ~P X )
16 15 sselda
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> x e. ~P X )
17 16 elpwid
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> x C_ X )
18 14 17 ssfid
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> x e. Fin )
19 hashen
 |-  ( ( Y e. Fin /\ x e. Fin ) -> ( ( # ` Y ) = ( # ` x ) <-> Y ~~ x ) )
20 13 18 19 syl2anc
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> ( ( # ` Y ) = ( # ` x ) <-> Y ~~ x ) )
21 9 20 mpbird
 |-  ( ( ph /\ x e. ( X /. .~ ) ) -> ( # ` Y ) = ( # ` x ) )
22 21 sumeq2dv
 |-  ( ph -> sum_ x e. ( X /. .~ ) ( # ` Y ) = sum_ x e. ( X /. .~ ) ( # ` x ) )
23 pwfi
 |-  ( X e. Fin <-> ~P X e. Fin )
24 4 23 sylib
 |-  ( ph -> ~P X e. Fin )
25 24 15 ssfid
 |-  ( ph -> ( X /. .~ ) e. Fin )
26 hashcl
 |-  ( Y e. Fin -> ( # ` Y ) e. NN0 )
27 12 26 syl
 |-  ( ph -> ( # ` Y ) e. NN0 )
28 27 nn0cnd
 |-  ( ph -> ( # ` Y ) e. CC )
29 fsumconst
 |-  ( ( ( X /. .~ ) e. Fin /\ ( # ` Y ) e. CC ) -> sum_ x e. ( X /. .~ ) ( # ` Y ) = ( ( # ` ( X /. .~ ) ) x. ( # ` Y ) ) )
30 25 28 29 syl2anc
 |-  ( ph -> sum_ x e. ( X /. .~ ) ( # ` Y ) = ( ( # ` ( X /. .~ ) ) x. ( # ` Y ) ) )
31 7 22 30 3eqtr2d
 |-  ( ph -> ( # ` X ) = ( ( # ` ( X /. .~ ) ) x. ( # ` Y ) ) )