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