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 O = od G
Assertion odsubdvds S SubGrp G S Fin A S O A S

Proof

Step Hyp Ref Expression
1 odsubdvds.1 O = od G
2 eqid G 𝑠 S = G 𝑠 S
3 2 subggrp S SubGrp G G 𝑠 S Grp
4 3 3ad2ant1 S SubGrp G S Fin A S G 𝑠 S Grp
5 2 subgbas S SubGrp G S = Base G 𝑠 S
6 5 3ad2ant1 S SubGrp G S Fin A S S = Base G 𝑠 S
7 simp2 S SubGrp G S Fin A S S Fin
8 6 7 eqeltrrd S SubGrp G S Fin A S Base G 𝑠 S Fin
9 simp3 S SubGrp G S Fin A S A S
10 9 6 eleqtrd S SubGrp G S Fin A S A Base G 𝑠 S
11 eqid Base G 𝑠 S = Base G 𝑠 S
12 eqid od G 𝑠 S = od G 𝑠 S
13 11 12 oddvds2 G 𝑠 S Grp Base G 𝑠 S Fin A Base G 𝑠 S od G 𝑠 S A Base G 𝑠 S
14 4 8 10 13 syl3anc S SubGrp G S Fin A S od G 𝑠 S A Base G 𝑠 S
15 2 1 12 subgod S SubGrp G A S O A = od G 𝑠 S A
16 15 3adant2 S SubGrp G S Fin A S O A = od G 𝑠 S A
17 6 fveq2d S SubGrp G S Fin A S S = Base G 𝑠 S
18 14 16 17 3brtr4d S SubGrp G S Fin A S O A S