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 ∧ 𝐴𝑆 ) → ( 𝑂𝐴 ) ∥ ( ♯ ‘ 𝑆 ) )