Theorem subgod

Description: The order of an element is the same in a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015) (Proof shortened by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	submod.h	|- H = ( G |`s Y )
	submod.o	|- O = ( od ` G )
	submod.p	|- P = ( od ` H )
Assertion	subgod	|- ( ( Y e. ( SubGrp ` G ) /\ A e. Y ) -> ( O ` A ) = ( P ` A ) )

Proof

Step	Hyp	Ref	Expression
1		submod.h	|- H = ( G |`s Y )
2		submod.o	|- O = ( od ` G )
3		submod.p	|- P = ( od ` H )
4		subgsubm	|- ( Y e. ( SubGrp ` G ) -> Y e. ( SubMnd ` G ) )
5	1 2 3	submod	|- ( ( Y e. ( SubMnd ` G ) /\ A e. Y ) -> ( O ` A ) = ( P ` A ) )
6	4 5	sylan	|- ( ( Y e. ( SubGrp ` G ) /\ A e. Y ) -> ( O ` A ) = ( P ` A ) )