Metamath Proof Explorer

Theorem ballotlemirc

Description: Applying R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017) (Revised by AV, 6-Oct-2020)

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
Assertion ballotlemirc ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = ( 𝐼 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 1 2 3 4 5 6 7 8 9 10 ballotlemrc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑅 ‘ 𝐶 ) ∈ ( 𝑂 ∖ 𝐸 ) )
12 1 2 3 4 5 6 7 8 ballotlemi ⊢ ( ( 𝑅 ‘ 𝐶 ) ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
13 11 12 syl ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
14 ltso ⊢ < Or ℝ
15 14 a1i ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → < Or ℝ )
16 1 2 3 4 5 6 7 8 ballotlemiex ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ 𝐶 ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
17 16 simpld ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
18 17 elfzelzd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℤ )
19 18 zred ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ ℝ )
20 eqid ⊢ ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) ) = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
21 1 2 3 4 5 6 7 8 9 10 20 ballotlemfrci ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 )
22 fveqeq2 ⊢ ( 𝑘 = ( 𝐼 ‘ 𝐶 ) → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
23 22 elrab ⊢ ( ( 𝐼 ‘ 𝐶 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ↔ ( ( 𝐼 ‘ 𝐶 ) ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ ( 𝐼 ‘ 𝐶 ) ) = 0 ) )
24 17 21 23 sylanbrc ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } )
25 elrabi ⊢ ( 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } → 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
26 25 anim2i ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ) → ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) )
27 simpr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → 𝑦 < ( 𝐼 ‘ 𝐶 ) )
28 1 2 3 4 5 6 7 8 9 10 ballotlemfrcn0 ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑦 ) ≠ 0 )
29 28 neneqd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → ¬ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑦 ) = 0 )
30 fveqeq2 ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑦 ) = 0 ) )
31 30 elrab ⊢ ( 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ↔ ( 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑦 ) = 0 ) )
32 31 simprbi ⊢ ( 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } → ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑦 ) = 0 )
33 29 32 nsyl ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → ¬ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } )
34 33 3expa ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → ¬ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } )
35 27 34 syldan ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) → ¬ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } )
36 35 ex ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝑦 < ( 𝐼 ‘ 𝐶 ) → ¬ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ) )
37 36 con2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } → ¬ 𝑦 < ( 𝐼 ‘ 𝐶 ) ) )
38 37 imp ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ) → ¬ 𝑦 < ( 𝐼 ‘ 𝐶 ) )
39 26 38 sylancom ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑦 ∈ { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } ) → ¬ 𝑦 < ( 𝐼 ‘ 𝐶 ) )
40 15 19 24 39 infmin ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ ( 𝑅 ‘ 𝐶 ) ) ‘ 𝑘 ) = 0 } , ℝ , < ) = ( 𝐼 ‘ 𝐶 ) )
41 13 40 eqtrd ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐶 ) ) = ( 𝐼 ‘ 𝐶 ) )