This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odsubdvds

Description: The order of an element of a subgroup divides the order of the subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis odsubdvds.1 
|- O = ( od ` G )
Assertion odsubdvds 
|- ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( O ` A ) || ( # ` S ) )

Proof

Step Hyp Ref Expression
1 odsubdvds.1 
 |-  O = ( od ` G )
2 eqid 
 |-  ( G |`s S ) = ( G |`s S )
3 2 subggrp 
 |-  ( S e. ( SubGrp ` G ) -> ( G |`s S ) e. Grp )
4 3 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( G |`s S ) e. Grp )
5 2 subgbas 
 |-  ( S e. ( SubGrp ` G ) -> S = ( Base ` ( G |`s S ) ) )
6 5 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> S = ( Base ` ( G |`s S ) ) )
7 simp2 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> S e. Fin )
8 6 7 eqeltrrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( Base ` ( G |`s S ) ) e. Fin )
9 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> A e. S )
10 9 6 eleqtrd 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> A e. ( Base ` ( G |`s S ) ) )
11 eqid 
 |-  ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
12 eqid 
 |-  ( od ` ( G |`s S ) ) = ( od ` ( G |`s S ) )
13 11 12 oddvds2 
 |-  ( ( ( G |`s S ) e. Grp /\ ( Base ` ( G |`s S ) ) e. Fin /\ A e. ( Base ` ( G |`s S ) ) ) -> ( ( od ` ( G |`s S ) ) ` A ) || ( # ` ( Base ` ( G |`s S ) ) ) )
14 4 8 10 13 syl3anc 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( ( od ` ( G |`s S ) ) ` A ) || ( # ` ( Base ` ( G |`s S ) ) ) )
15 2 1 12 subgod 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. S ) -> ( O ` A ) = ( ( od ` ( G |`s S ) ) ` A ) )
16 15 3adant2 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( O ` A ) = ( ( od ` ( G |`s S ) ) ` A ) )
17 6 fveq2d 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( # ` S ) = ( # ` ( Base ` ( G |`s S ) ) ) )
18 14 16 17 3brtr4d 
 |-  ( ( S e. ( SubGrp ` G ) /\ S e. Fin /\ A e. S ) -> ( O ` A ) || ( # ` S ) )