Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	lagsubg	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑌 ) ∥ ( ♯ ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lagsubg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		simpr	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → 𝑋 ∈ Fin )
3		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
4	2 3	sylib	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → 𝒫 𝑋 ∈ Fin )
5		eqid	⊢ ( 𝐺 ~QG 𝑌 ) = ( 𝐺 ~QG 𝑌 )
6	1 5	eqger	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑌 ) Er 𝑋 )
7	6	adantr	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( 𝐺 ~QG 𝑌 ) Er 𝑋 )
8	7	qsss	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ⊆ 𝒫 𝑋 )
9	4 8	ssfid	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ∈ Fin )
10		hashcl	⊢ ( ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) ∈ ℕ0 )
11	9 10	syl	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) ∈ ℕ0 )
12	11	nn0zd	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) ∈ ℤ )
13		id	⊢ ( 𝑋 ∈ Fin → 𝑋 ∈ Fin )
14	1	subgss	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝑌 ⊆ 𝑋 )
15		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 ∈ Fin )
16	13 14 15	syl2anr	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → 𝑌 ∈ Fin )
17		hashcl	⊢ ( 𝑌 ∈ Fin → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
18	16 17	syl	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑌 ) ∈ ℕ0 )
19	18	nn0zd	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑌 ) ∈ ℤ )
20		dvdsmul2	⊢ ( ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) ∈ ℤ ∧ ( ♯ ‘ 𝑌 ) ∈ ℤ ) → ( ♯ ‘ 𝑌 ) ∥ ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) · ( ♯ ‘ 𝑌 ) ) )
21	12 19 20	syl2anc	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑌 ) ∥ ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) · ( ♯ ‘ 𝑌 ) ) )
22		simpl	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
23	1 5 22 2	lagsubg2	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ ( 𝑋 / ( 𝐺 ~QG 𝑌 ) ) ) · ( ♯ ‘ 𝑌 ) ) )
24	21 23	breqtrrd	⊢ ( ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑌 ) ∥ ( ♯ ‘ 𝑋 ) )