Metamath Proof Explorer


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𝑠Y
submod.o O=odG
submod.p P=odH
Assertion subgod YSubGrpGAYOA=PA

Proof

Step Hyp Ref Expression
1 submod.h H=G𝑠Y
2 submod.o O=odG
3 submod.p P=odH
4 subgsubm YSubGrpGYSubMndG
5 1 2 3 submod YSubMndGAYOA=PA
6 4 5 sylan YSubGrpGAYOA=PA