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 ⊢ X = Base G
Assertion lagsubg ⊢ Y ∈ SubGrp ⁡ G ∧ X ∈ Fin → Y ∥ X

Proof

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