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 \in SubGrp (G) \land S \in Fin \land A \in S) \to O (A) ∥ \|S\|$

Proof

Step	Hyp	Ref	Expression
1		odsubdvds.1	$⊢ O = od (G)$
2		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
3	2	subggrp	$⊢ S \in SubGrp (G) \to G ↾_{𝑠} S \in Grp$
4	3	3ad2ant1	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to G ↾_{𝑠} S \in Grp$
5	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{(G ↾_{𝑠} S)}$
6	5	3ad2ant1	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to S = {Base}_{(G ↾_{𝑠} S)}$
7		simp2	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to S \in Fin$
8	6 7	eqeltrrd	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to {Base}_{(G ↾_{𝑠} S)} \in Fin$
9		simp3	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to A \in S$
10	9 6	eleqtrd	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to A \in {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 \in Grp \land {Base}_{(G ↾_{𝑠} S)} \in Fin \land A \in {Base}_{(G ↾_{𝑠} S)}) \to od (G ↾_{𝑠} S) (A) ∥ \|{Base}_{(G ↾_{𝑠} S)}\|$
14	4 8 10 13	syl3anc	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to od (G ↾_{𝑠} S) (A) ∥ \|{Base}_{(G ↾_{𝑠} S)}\|$
15	2 1 12	subgod	$⊢ (S \in SubGrp (G) \land A \in S) \to O (A) = od (G ↾_{𝑠} S) (A)$
16	15	3adant2	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to O (A) = od (G ↾_{𝑠} S) (A)$
17	6	fveq2d	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to \|S\| = \|{Base}_{(G ↾_{𝑠} S)}\|$
18	14 16 17	3brtr4d	$⊢ (S \in SubGrp (G) \land S \in Fin \land A \in S) \to O (A) ∥ \|S\|$