Metamath Proof Explorer

Theorem ballotlemi

Description: Value of I for a given counting C . (Contributed by Thierry Arnoux, 1-Dec-2016) (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 } , ℝ , < ) )
Assertion ballotlemi ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )

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 fveq2 ⊢ ( 𝑑 = 𝐶 → ( 𝐹 ‘ 𝑑 ) = ( 𝐹 ‘ 𝐶 ) )
10 9 fveq1d ⊢ ( 𝑑 = 𝐶 → ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) )
11 10 eqeq1d ⊢ ( 𝑑 = 𝐶 → ( ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 ) )
12 11 rabbidv ⊢ ( 𝑑 = 𝐶 → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } = { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } )
13 12 infeq1d ⊢ ( 𝑑 = 𝐶 → inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } , ℝ , < ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
14 fveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑑 ) )
15 14 fveq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) )
16 15 eqeq1d ⊢ ( 𝑐 = 𝑑 → ( ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 ↔ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 ) )
17 16 rabbidv ⊢ ( 𝑐 = 𝑑 → { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } = { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } )
18 17 infeq1d ⊢ ( 𝑐 = 𝑑 → inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
19 18 cbvmptv ⊢ ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ) = ( 𝑑 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
20 8 19 eqtri ⊢ 𝐼 = ( 𝑑 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑑 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
21 ltso ⊢ < Or ℝ
22 21 infex ⊢ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) ∈ V
23 13 20 22 fvmpt ⊢ ( 𝐶 ∈ ( 𝑂 ∖ 𝐸 ) → ( 𝐼 ‘ 𝐶 ) = inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝐶 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )