This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝐻 = ( 𝐺 ↾_s 𝑌 )
	submod.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	submod.p	⊢ 𝑃 = ( od ‘ 𝐻 )
Assertion	subgod	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		submod.h	⊢ 𝐻 = ( 𝐺 ↾_s 𝑌 )
2		submod.o	⊢ 𝑂 = ( od ‘ 𝐺 )
3		submod.p	⊢ 𝑃 = ( od ‘ 𝐻 )
4		subgsubm	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ∈ ( SubMnd ‘ 𝐺 ) )
5	1 2 3	submod	⊢ ( ( 𝑌 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )
6	4 5	sylan	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐴 ) )