This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) → ( ♯ ‘ 𝑌 ) ∥ ( ♯ ‘ 𝑋 ) )