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=BaseG
sylow1.g ⊢φ→G∈Grp
sylow1.f ⊢φ→X∈Fin
sylow1.p ⊢φ→P∈ℙ
sylow1.n ⊢φ→N∈ℕ0
sylow1.d ⊢φ→PN∥X
Assertion sylow1 ⊢φ→∃g∈SubGrp⁡Gg=PN

Proof

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