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 ) )