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

Metamath Proof Explorer

Theorem odsubdvds

Description: The order of an element of a subgroup divides the order of the subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis odsubdvds.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion odsubdvds ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 odsubdvds.1 ⊢ 𝑂 = ( od ‘ 𝐺 )
2 eqid ⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
3 2 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
4 3 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
5 2 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
7 simp2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → 𝑆 ∈ Fin )
8 6 7 eqeltrrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∈ Fin )
9 simp3 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
10 9 6 eleqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
11 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
12 eqid ⊢ ( od ‘ ( 𝐺 ↾s 𝑆 ) ) = ( od ‘ ( 𝐺 ↾s 𝑆 ) )
13 11 12 oddvds2 ⊢ ( ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∈ Fin ∧ 𝐴 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) → ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) )
14 4 8 10 13 syl3anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝐴 ) ∥ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) )
15 2 1 12 subgod ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑂 ‘ 𝐴 ) = ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝐴 ) )
16 15 3adant2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( 𝑂 ‘ 𝐴 ) = ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝐴 ) )
17 6 fveq2d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) )
18 14 16 17 3brtr4d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆 ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ♯ ‘ 𝑆 ) )