Metamath Proof Explorer

Theorem ballotlemieq

Description: If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
Assertion ballotlemieq ⊢C∈O∖E∧D∈O∖E∧I⁡C=I⁡D→S⁡C=S⁡D

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 simpl ⊢I⁡C=I⁡D∧i∈1…M+N→I⁡C=I⁡D
11 10 breq2d ⊢I⁡C=I⁡D∧i∈1…M+N→i≤I⁡C↔i≤I⁡D
12 10 oveq1d ⊢I⁡C=I⁡D∧i∈1…M+N→I⁡C+1=I⁡D+1
13 12 oveq1d ⊢I⁡C=I⁡D∧i∈1…M+N→I⁡C+1-i=I⁡D+1-i
14 11 13 ifbieq1d ⊢I⁡C=I⁡D∧i∈1…M+N→ifi≤I⁡CI⁡C+1-ii=ifi≤I⁡DI⁡D+1-ii
15 14 mpteq2dva ⊢I⁡C=I⁡D→i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii=i∈1…M+N⟼ifi≤I⁡DI⁡D+1-ii
16 15 3ad2ant3 ⊢C∈O∖E∧D∈O∖E∧I⁡C=I⁡D→i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii=i∈1…M+N⟼ifi≤I⁡DI⁡D+1-ii
17 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢C∈O∖E→S⁡C=i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii
18 17 3ad2ant1 ⊢C∈O∖E∧D∈O∖E∧I⁡C=I⁡D→S⁡C=i∈1…M+N⟼ifi≤I⁡CI⁡C+1-ii
19 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢D∈O∖E→S⁡D=i∈1…M+N⟼ifi≤I⁡DI⁡D+1-ii
20 19 3ad2ant2 ⊢C∈O∖E∧D∈O∖E∧I⁡C=I⁡D→S⁡D=i∈1…M+N⟼ifi≤I⁡DI⁡D+1-ii
21 16 18 20 3eqtr4d ⊢C∈O∖E∧D∈O∖E∧I⁡C=I⁡D→S⁡C=S⁡D