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 ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
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 → if i ≤ I ⁡ C I ⁡ C + 1 - i i = if i ≤ I ⁡ D I ⁡ D + 1 - i i
15 14 mpteq2dva ⊢ I ⁡ C = I ⁡ D → i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ D I ⁡ D + 1 - i i
16 15 3ad2ant3 ⊢ C ∈ O ∖ E ∧ D ∈ O ∖ E ∧ I ⁡ C = I ⁡ D → i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ D I ⁡ D + 1 - i i
17 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢ C ∈ O ∖ E → S ⁡ C = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i
18 17 3ad2ant1 ⊢ C ∈ O ∖ E ∧ D ∈ O ∖ E ∧ I ⁡ C = I ⁡ D → S ⁡ C = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ C I ⁡ C + 1 - i i
19 1 2 3 4 5 6 7 8 9 ballotlemsval ⊢ D ∈ O ∖ E → S ⁡ D = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ D I ⁡ D + 1 - i i
20 19 3ad2ant2 ⊢ C ∈ O ∖ E ∧ D ∈ O ∖ E ∧ I ⁡ C = I ⁡ D → S ⁡ D = i ∈ 1 … M + N ⟼ if i ≤ I ⁡ D I ⁡ D + 1 - i i
21 16 18 20 3eqtr4d ⊢ C ∈ O ∖ E ∧ D ∈ O ∖ E ∧ I ⁡ C = I ⁡ D → S ⁡ C = S ⁡ D