Metamath Proof Explorer

Theorem sylow1

Description: Sylow's first theorem. If P ^ N is a prime power that divides the cardinality of G , then G has a supgroup with size P ^ N . This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypotheses sylow1.x ⊢ X = Base G
sylow1.g ⊢ φ → G ∈ Grp
sylow1.f ⊢ φ → X ∈ Fin
sylow1.p ⊢ φ → P ∈ ℙ
sylow1.n ⊢ φ → N ∈ ℕ 0
sylow1.d ⊢ φ → P N ∥ X
Assertion sylow1 ⊢ φ → ∃ g ∈ SubGrp ⁡ G g = P N

Proof

Step Hyp Ref Expression
1 sylow1.x ⊢ X = Base G
2 sylow1.g ⊢ φ → G ∈ Grp
3 sylow1.f ⊢ φ → X ∈ Fin
4 sylow1.p ⊢ φ → P ∈ ℙ
5 sylow1.n ⊢ φ → N ∈ ℕ 0
6 sylow1.d ⊢ φ → P N ∥ X
7 eqid ⊢ + G = + G
8 eqid ⊢ s ∈ 𝒫 X | s = P N = s ∈ 𝒫 X | s = P N
9 oveq2 ⊢ s = z → u + G s = u + G z
10 9 cbvmptv ⊢ s ∈ v ⟼ u + G s = z ∈ v ⟼ u + G z
11 oveq1 ⊢ u = x → u + G z = x + G z
12 11 mpteq2dv ⊢ u = x → z ∈ v ⟼ u + G z = z ∈ v ⟼ x + G z
13 10 12 eqtrid ⊢ u = x → s ∈ v ⟼ u + G s = z ∈ v ⟼ x + G z
14 13 rneqd ⊢ u = x → ran ⁡ s ∈ v ⟼ u + G s = ran ⁡ z ∈ v ⟼ x + G z
15 mpteq1 ⊢ v = y → z ∈ v ⟼ x + G z = z ∈ y ⟼ x + G z
16 15 rneqd ⊢ v = y → ran ⁡ z ∈ v ⟼ x + G z = ran ⁡ z ∈ y ⟼ x + G z
17 14 16 cbvmpov ⊢ u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s = x ∈ X , y ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ z ∈ y ⟼ x + G z
18 preq12 ⊢ a = x ∧ b = y → a b = x y
19 18 sseq1d ⊢ a = x ∧ b = y → a b ⊆ s ∈ 𝒫 X | s = P N ↔ x y ⊆ s ∈ 𝒫 X | s = P N
20 oveq2 ⊢ a = x → k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s x
21 id ⊢ b = y → b = y
22 20 21 eqeqan12d ⊢ a = x ∧ b = y → k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ↔ k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s x = y
23 22 rexbidv ⊢ a = x ∧ b = y → ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ↔ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s x = y
24 19 23 anbi12d ⊢ a = x ∧ b = y → a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ↔ x y ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s x = y
25 24 cbvopabv ⊢ a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b = x y | x y ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s x = y
26 1 2 3 4 5 6 7 8 17 25 sylow1lem3 ⊢ φ → ∃ h ∈ s ∈ 𝒫 X | s = P N P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N
27 2 adantr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → G ∈ Grp
28 3 adantr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → X ∈ Fin
29 4 adantr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → P ∈ ℙ
30 5 adantr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → N ∈ ℕ 0
31 6 adantr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → P N ∥ X
32 simprl ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → h ∈ s ∈ 𝒫 X | s = P N
33 eqid ⊢ t ∈ X | t u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s h = h = t ∈ X | t u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s h = h
34 simprr ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N
35 1 27 28 29 30 31 7 8 17 25 32 33 34 sylow1lem5 ⊢ φ ∧ h ∈ s ∈ 𝒫 X | s = P N ∧ P pCnt h a b | a b ⊆ s ∈ 𝒫 X | s = P N ∧ ∃ k ∈ X k u ∈ X , v ∈ s ∈ 𝒫 X | s = P N ⟼ ran ⁡ s ∈ v ⟼ u + G s a = b ≤ P pCnt X − N → ∃ g ∈ SubGrp ⁡ G g = P N
36 26 35 rexlimddv ⊢ φ → ∃ g ∈ SubGrp ⁡ G g = P N