Metamath Proof Explorer

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