Metamath Proof Explorer


Theorem sylow3

Description: Sylow's third theorem. The number of Sylow subgroups is a divisor of | G | / d , where d is the common order of a Sylow subgroup, and is equivalent to 1 mod P . This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 𝑋 = ( Base ‘ 𝐺 )
sylow3.g ( 𝜑𝐺 ∈ Grp )
sylow3.xf ( 𝜑𝑋 ∈ Fin )
sylow3.p ( 𝜑𝑃 ∈ ℙ )
sylow3.n 𝑁 = ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) )
Assertion sylow3 ( 𝜑 → ( 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∧ ( 𝑁 mod 𝑃 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 sylow3.x 𝑋 = ( Base ‘ 𝐺 )
2 sylow3.g ( 𝜑𝐺 ∈ Grp )
3 sylow3.xf ( 𝜑𝑋 ∈ Fin )
4 sylow3.p ( 𝜑𝑃 ∈ ℙ )
5 sylow3.n 𝑁 = ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) )
6 1 slwn0 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ ) → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )
7 2 3 4 6 syl3anc ( 𝜑 → ( 𝑃 pSyl 𝐺 ) ≠ ∅ )
8 n0 ( ( 𝑃 pSyl 𝐺 ) ≠ ∅ ↔ ∃ 𝑘 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) )
9 7 8 sylib ( 𝜑 → ∃ 𝑘 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) )
10 2 adantr ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝐺 ∈ Grp )
11 3 adantr ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑋 ∈ Fin )
12 4 adantr ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑃 ∈ ℙ )
13 eqid ( +g𝐺 ) = ( +g𝐺 )
14 eqid ( -g𝐺 ) = ( -g𝐺 )
15 oveq2 ( 𝑐 = 𝑧 → ( 𝑎 ( +g𝐺 ) 𝑐 ) = ( 𝑎 ( +g𝐺 ) 𝑧 ) )
16 15 oveq1d ( 𝑐 = 𝑧 → ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) = ( ( 𝑎 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑎 ) )
17 16 cbvmptv ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) = ( 𝑧𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑎 ) )
18 oveq1 ( 𝑎 = 𝑥 → ( 𝑎 ( +g𝐺 ) 𝑧 ) = ( 𝑥 ( +g𝐺 ) 𝑧 ) )
19 id ( 𝑎 = 𝑥𝑎 = 𝑥 )
20 18 19 oveq12d ( 𝑎 = 𝑥 → ( ( 𝑎 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑎 ) = ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) )
21 20 mpteq2dv ( 𝑎 = 𝑥 → ( 𝑧𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑎 ) ) = ( 𝑧𝑏 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
22 17 21 syl5eq ( 𝑎 = 𝑥 → ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) = ( 𝑧𝑏 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
23 22 rneqd ( 𝑎 = 𝑥 → ran ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) = ran ( 𝑧𝑏 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
24 mpteq1 ( 𝑏 = 𝑦 → ( 𝑧𝑏 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) = ( 𝑧𝑦 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
25 24 rneqd ( 𝑏 = 𝑦 → ran ( 𝑧𝑏 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) = ran ( 𝑧𝑦 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
26 23 25 cbvmpov ( 𝑎𝑋 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) ) = ( 𝑥𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧𝑦 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
27 simpr ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) )
28 eqid { 𝑢𝑋 ∣ ( 𝑢 ( 𝑎𝑋 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) ) 𝑘 ) = 𝑘 } = { 𝑢𝑋 ∣ ( 𝑢 ( 𝑎𝑋 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) ) 𝑘 ) = 𝑘 }
29 eqid { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑘 ↔ ( 𝑦 ( +g𝐺 ) 𝑥 ) ∈ 𝑘 ) } = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑘 ↔ ( 𝑦 ( +g𝐺 ) 𝑥 ) ∈ 𝑘 ) }
30 1 10 11 12 13 14 26 27 28 29 sylow3lem4 ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
31 5 30 eqbrtrid ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
32 5 oveq1i ( 𝑁 mod 𝑃 ) = ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 )
33 23 25 cbvmpov ( 𝑎𝑘 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐𝑏 ↦ ( ( 𝑎 ( +g𝐺 ) 𝑐 ) ( -g𝐺 ) 𝑎 ) ) ) = ( 𝑥𝑘 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧𝑦 ↦ ( ( 𝑥 ( +g𝐺 ) 𝑧 ) ( -g𝐺 ) 𝑥 ) ) )
34 eqid { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 ( +g𝐺 ) 𝑥 ) ∈ 𝑠 ) } = { 𝑥𝑋 ∣ ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝐺 ) 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 ( +g𝐺 ) 𝑥 ) ∈ 𝑠 ) }
35 1 10 11 12 13 14 27 33 34 sylow3lem6 ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( ( ♯ ‘ ( 𝑃 pSyl 𝐺 ) ) mod 𝑃 ) = 1 )
36 32 35 syl5eq ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝑁 mod 𝑃 ) = 1 )
37 31 36 jca ( ( 𝜑𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∧ ( 𝑁 mod 𝑃 ) = 1 ) )
38 9 37 exlimddv ( 𝜑 → ( 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∧ ( 𝑁 mod 𝑃 ) = 1 ) )