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 = od G
submod.p P = od H
Assertion subgod Y SubGrp G A Y O A = P A

Proof

Step Hyp Ref Expression
1 submod.h H = G 𝑠 Y
2 submod.o O = od G
3 submod.p P = od H
4 subgsubm Y SubGrp G Y SubMnd G
5 1 2 3 submod Y SubMnd G A Y O A = P A
6 4 5 sylan Y SubGrp G A Y O A = P A