Metamath Proof Explorer


Theorem lagsubg

Description: Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis lagsubg.1
|- X = ( Base ` G )
Assertion lagsubg
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) || ( # ` X ) )

Proof

Step Hyp Ref Expression
1 lagsubg.1
 |-  X = ( Base ` G )
2 simpr
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> X e. Fin )
3 pwfi
 |-  ( X e. Fin <-> ~P X e. Fin )
4 2 3 sylib
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ~P X e. Fin )
5 eqid
 |-  ( G ~QG Y ) = ( G ~QG Y )
6 1 5 eqger
 |-  ( Y e. ( SubGrp ` G ) -> ( G ~QG Y ) Er X )
7 6 adantr
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( G ~QG Y ) Er X )
8 7 qsss
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( X /. ( G ~QG Y ) ) C_ ~P X )
9 4 8 ssfid
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( X /. ( G ~QG Y ) ) e. Fin )
10 hashcl
 |-  ( ( X /. ( G ~QG Y ) ) e. Fin -> ( # ` ( X /. ( G ~QG Y ) ) ) e. NN0 )
11 9 10 syl
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` ( X /. ( G ~QG Y ) ) ) e. NN0 )
12 11 nn0zd
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` ( X /. ( G ~QG Y ) ) ) e. ZZ )
13 id
 |-  ( X e. Fin -> X e. Fin )
14 1 subgss
 |-  ( Y e. ( SubGrp ` G ) -> Y C_ X )
15 ssfi
 |-  ( ( X e. Fin /\ Y C_ X ) -> Y e. Fin )
16 13 14 15 syl2anr
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> Y e. Fin )
17 hashcl
 |-  ( Y e. Fin -> ( # ` Y ) e. NN0 )
18 16 17 syl
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) e. NN0 )
19 18 nn0zd
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) e. ZZ )
20 dvdsmul2
 |-  ( ( ( # ` ( X /. ( G ~QG Y ) ) ) e. ZZ /\ ( # ` Y ) e. ZZ ) -> ( # ` Y ) || ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) )
21 12 19 20 syl2anc
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) || ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) )
22 simpl
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> Y e. ( SubGrp ` G ) )
23 1 5 22 2 lagsubg2
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) )
24 21 23 breqtrrd
 |-  ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) || ( # ` X ) )