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