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