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 𝑋 = ( Base ‘ 𝐺 )
sylow1.g ( 𝜑𝐺 ∈ Grp )
sylow1.f ( 𝜑𝑋 ∈ Fin )
sylow1.p ( 𝜑𝑃 ∈ ℙ )
sylow1.n ( 𝜑𝑁 ∈ ℕ0 )
sylow1.d ( 𝜑 → ( 𝑃𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
Assertion sylow1 ( 𝜑 → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃𝑁 ) )

Proof

Step Hyp Ref Expression
1 sylow1.x 𝑋 = ( Base ‘ 𝐺 )
2 sylow1.g ( 𝜑𝐺 ∈ Grp )
3 sylow1.f ( 𝜑𝑋 ∈ Fin )
4 sylow1.p ( 𝜑𝑃 ∈ ℙ )
5 sylow1.n ( 𝜑𝑁 ∈ ℕ0 )
6 sylow1.d ( 𝜑 → ( 𝑃𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7 eqid ( +g𝐺 ) = ( +g𝐺 )
8 eqid { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) }
9 oveq2 ( 𝑠 = 𝑧 → ( 𝑢 ( +g𝐺 ) 𝑠 ) = ( 𝑢 ( +g𝐺 ) 𝑧 ) )
10 9 cbvmptv ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) = ( 𝑧𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑧 ) )
11 oveq1 ( 𝑢 = 𝑥 → ( 𝑢 ( +g𝐺 ) 𝑧 ) = ( 𝑥 ( +g𝐺 ) 𝑧 ) )
12 11 mpteq2dv ( 𝑢 = 𝑥 → ( 𝑧𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑧 ) ) = ( 𝑧𝑣 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
13 10 12 syl5eq ( 𝑢 = 𝑥 → ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) = ( 𝑧𝑣 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
14 13 rneqd ( 𝑢 = 𝑥 → ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) = ran ( 𝑧𝑣 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
15 mpteq1 ( 𝑣 = 𝑦 → ( 𝑧𝑣 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) = ( 𝑧𝑦 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
16 15 rneqd ( 𝑣 = 𝑦 → ran ( 𝑧𝑣 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) = ran ( 𝑧𝑦 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
17 14 16 cbvmpov ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) = ( 𝑥𝑋 , 𝑦 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑧𝑦 ↦ ( 𝑥 ( +g𝐺 ) 𝑧 ) ) )
18 preq12 ( ( 𝑎 = 𝑥𝑏 = 𝑦 ) → { 𝑎 , 𝑏 } = { 𝑥 , 𝑦 } )
19 18 sseq1d ( ( 𝑎 = 𝑥𝑏 = 𝑦 ) → ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↔ { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ) )
20 oveq2 ( 𝑎 = 𝑥 → ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑥 ) )
21 id ( 𝑏 = 𝑦𝑏 = 𝑦 )
22 20 21 eqeqan12d ( ( 𝑎 = 𝑥𝑏 = 𝑦 ) → ( ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) )
23 22 rexbidv ( ( 𝑎 = 𝑥𝑏 = 𝑦 ) → ( ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ↔ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) )
24 19 23 anbi12d ( ( 𝑎 = 𝑥𝑏 = 𝑦 ) → ( ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) ↔ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) ) )
25 24 cbvopabv { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑥 ) = 𝑦 ) }
26 1 2 3 4 5 6 7 8 17 25 sylow1lem3 ( 𝜑 → ∃ ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
27 2 adantr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝐺 ∈ Grp )
28 3 adantr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑋 ∈ Fin )
29 4 adantr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑃 ∈ ℙ )
30 5 adantr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
31 6 adantr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
32 simprl ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } )
33 eqid { 𝑡𝑋 ∣ ( 𝑡 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) ) = } = { 𝑡𝑋 ∣ ( 𝑡 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) ) = }
34 simprr ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
35 1 27 28 29 30 31 7 8 17 25 32 33 34 sylow1lem5 ( ( 𝜑 ∧ ( ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ( 𝑃 pCnt ( ♯ ‘ [ ] { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( { 𝑎 , 𝑏 } ⊆ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ∧ ∃ 𝑘𝑋 ( 𝑘 ( 𝑢𝑋 , 𝑣 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃𝑁 ) } ↦ ran ( 𝑠𝑣 ↦ ( 𝑢 ( +g𝐺 ) 𝑠 ) ) ) 𝑎 ) = 𝑏 ) } ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) ) → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃𝑁 ) )
36 26 35 rexlimddv ( 𝜑 → ∃ 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ 𝑔 ) = ( 𝑃𝑁 ) )