lagsubg

Description: Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Hypothesis	lagsubg.1	$⊢ X = {Base}_{G}$
	Assertion	lagsubg	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|Y\| ∥ \|X\|$

Proof

Step	Hyp	Ref	Expression
1		lagsubg.1	$⊢ X = {Base}_{G}$
2		simpr	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to X \in Fin$
3		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
4	2 3	sylib	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to 𝒫 X \in Fin$
5		eqid	$⊢ G ~_{QG} Y = G ~_{QG} Y$
6	1 5	eqger	$⊢ Y \in SubGrp (G) \to (G ~_{QG} Y) Er X$
7	6	adantr	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to (G ~_{QG} Y) Er X$
8	7	qsss	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to X / (G ~_{QG} Y) \subseteq 𝒫 X$
9	4 8	ssfid	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to X / (G ~_{QG} Y) \in Fin$
10		hashcl	$⊢ X / (G ~_{QG} Y) \in Fin \to \|X / (G ~_{QG} Y)\| \in ℕ_{0}$
11	9 10	syl	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|X / (G ~_{QG} Y)\| \in ℕ_{0}$
12	11	nn0zd	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|X / (G ~_{QG} Y)\| \in ℤ$
13		id	$⊢ X \in Fin \to X \in Fin$
14	1	subgss	$⊢ Y \in SubGrp (G) \to Y \subseteq X$
15		ssfi	$⊢ (X \in Fin \land Y \subseteq X) \to Y \in Fin$
16	13 14 15	syl2anr	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to Y \in Fin$
17		hashcl	$⊢ Y \in Fin \to \|Y\| \in ℕ_{0}$
18	16 17	syl	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|Y\| \in ℕ_{0}$
19	18	nn0zd	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|Y\| \in ℤ$
20		dvdsmul2	$⊢ (\|X / (G ~_{QG} Y)\| \in ℤ \land \|Y\| \in ℤ) \to \|Y\| ∥ \|X / (G ~_{QG} Y)\| \|Y\|$
21	12 19 20	syl2anc	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|Y\| ∥ \|X / (G ~_{QG} Y)\| \|Y\|$
22		simpl	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to Y \in SubGrp (G)$
23	1 5 22 2	lagsubg2	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|X\| = \|X / (G ~_{QG} Y)\| \|Y\|$
24	21 23	breqtrrd	$⊢ (Y \in SubGrp (G) \land X \in Fin) \to \|Y\| ∥ \|X\|$

Metamath Proof Explorer

Theorem lagsubg

Proof