Metamath Proof Explorer

Theorem ballotlemsv

Description: Value of S evaluated at J for a given counting C . (Contributed by Thierry Arnoux, 12-Apr-2017)

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 ) − 𝑖 ) , 𝑖 ) ) )
Assertion ballotlemsv ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )

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 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
11 breq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) ↔ 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ) )
12 oveq2 ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) )
13 id ⊢ ( 𝑖 = 𝑗 → 𝑖 = 𝑗 )
14 11 12 13 ifbieq12d ⊢ ( 𝑖 = 𝑗 → if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) = if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
15 14 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑖 ) , 𝑖 ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) )
16 10 15 eqtrdi ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) )
17 16 adantr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝑆 ‘ 𝐶 ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) ) )
18 simpr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
19 18 breq1d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 = 𝐽 ) → ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) ↔ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) )
20 18 oveq2d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 = 𝐽 ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) = ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) )
21 19 20 18 ifbieq12d ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝑗 = 𝐽 ) → if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
22 21 adantlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝑗 = 𝐽 ) → if ( 𝑗 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝑗 ) , 𝑗 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )
23 simpr ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) )
24 ovexd ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) ∈ V )
25 elex ⊢ ( 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝐽 ∈ V )
26 25 ad2antlr ⊢ ( ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) ∧ ¬ 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) ) → 𝐽 ∈ V )
27 24 26 ifclda ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) ∈ V )
28 17 22 23 27 fvmptd ⊢ ( ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) ∧ 𝐽 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐽 ) = if ( 𝐽 ≤ ( 𝐼 ‘ 𝐶 ) , ( ( ( 𝐼 ‘ 𝐶 ) + 1 ) − 𝐽 ) , 𝐽 ) )