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 \in SubGrp (G) \land A \in Y) \to 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 \in SubGrp (G) \to Y \in SubMnd (G)$
5	1 2 3	submod	$⊢ (Y \in SubMnd (G) \land A \in Y) \to O (A) = P (A)$
6	4 5	sylan	$⊢ (Y \in SubGrp (G) \land A \in Y) \to O (A) = P (A)$