Metamath Proof Explorer

Theorem ballotlemrv

Description: Value of R evaluated at J . (Contributed by Thierry Arnoux, 17-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 ⟼ inf 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
ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
Assertion ballotlemrv ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ R ⁡ C ↔ if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C

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 ⟼ inf 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 ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
11 simpl ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → C ∈ O ∖ E
12 1 2 3 4 5 6 7 8 9 ballotlemsf1o ⊢ C ∈ O ∖ E → S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N ∧ S ⁡ C -1 = S ⁡ C
13 12 simpld ⊢ C ∈ O ∖ E → S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N
14 f1ofun ⊢ S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N → Fun ⁡ S ⁡ C
15 11 13 14 3syl ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → Fun ⁡ S ⁡ C
16 simpr ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ 1 … M + N
17 f1odm ⊢ S ⁡ C : 1 … M + N ⟶ 1-1 onto 1 … M + N → dom ⁡ S ⁡ C = 1 … M + N
18 11 13 17 3syl ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → dom ⁡ S ⁡ C = 1 … M + N
19 16 18 eleqtrrd ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ dom ⁡ S ⁡ C
20 fvimacnv ⊢ Fun ⁡ S ⁡ C ∧ J ∈ dom ⁡ S ⁡ C → S ⁡ C ⁡ J ∈ C ↔ J ∈ S ⁡ C -1 C
21 15 19 20 syl2anc ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → S ⁡ C ⁡ J ∈ C ↔ J ∈ S ⁡ C -1 C
22 1 2 3 4 5 6 7 8 9 ballotlemsv ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → S ⁡ C ⁡ J = if J ≤ I ⁡ C I ⁡ C + 1 - J J
23 22 eleq1d ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → S ⁡ C ⁡ J ∈ C ↔ if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C
24 12 simprd ⊢ C ∈ O ∖ E → S ⁡ C -1 = S ⁡ C
25 24 imaeq1d ⊢ C ∈ O ∖ E → S ⁡ C -1 C = S ⁡ C C
26 1 2 3 4 5 6 7 8 9 10 ballotlemrval ⊢ C ∈ O ∖ E → R ⁡ C = S ⁡ C C
27 25 26 eqtr4d ⊢ C ∈ O ∖ E → S ⁡ C -1 C = R ⁡ C
28 27 eleq2d ⊢ C ∈ O ∖ E → J ∈ S ⁡ C -1 C ↔ J ∈ R ⁡ C
29 11 28 syl ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ S ⁡ C -1 C ↔ J ∈ R ⁡ C
30 21 23 29 3bitr3rd ⊢ C ∈ O ∖ E ∧ J ∈ 1 … M + N → J ∈ R ⁡ C ↔ if J ≤ I ⁡ C I ⁡ C + 1 - J J ∈ C