This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝑎 = 𝑥 → ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 ( +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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝑁 mod 𝑃 ) = 1 )
37 31 36 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑃 pSyl 𝐺 ) ) → ( 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∧ ( 𝑁 mod 𝑃 ) = 1 ) )
38 9 37 exlimddv ⊢ ( 𝜑 → ( 𝑁 ∥ ( ( ♯ ‘ 𝑋 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ∧ ( 𝑁 mod 𝑃 ) = 1 ) )