ballotlemrv

Description: Value of R evaluated at J . (Contributed by Thierry Arnoux, 17-Apr-2017)

	Ref	Expression
Hypotheses	ballotth.m	$⊢ M \in ℕ$
	ballotth.n	$⊢ N \in ℕ$
	ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
	ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
	ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
	ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
	ballotth.mgtn	$⊢ N < M$
	ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
	ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
	ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
Assertion	ballotlemrv	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to (J \in R (C) \leftrightarrow if (J \leq I (C), I (C) + 1 - J, J) \in C)$

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	$⊢ M \in ℕ$
2		ballotth.n	$⊢ N \in ℕ$
3		ballotth.o	$⊢ O = \{c \in 𝒫 (1 \dots M + N) \| \|c\| = M\}$
4		ballotth.p	$⊢ P = (x \in 𝒫 O ⟼ \frac{\|x\|}{\|O\|})$
5		ballotth.f	$⊢ F = (c \in O ⟼ (i \in ℤ ⟼ \|(1 \dots i) \cap c\| - \|(1 \dots i) ∖ c\|))$
6		ballotth.e	$⊢ E = \{c \in O \| \forall i \in (1 \dots M + N) 0 < F (c) (i)\}$
7		ballotth.mgtn	$⊢ N < M$
8		ballotth.i	$⊢ I = (c \in (O ∖ E) ⟼ sup (\{k \in (1 \dots M + N) \| F (c) (k) = 0\} ℝ <))$
9		ballotth.s	$⊢ S = (c \in (O ∖ E) ⟼ (i \in (1 \dots M + N) ⟼ if (i \leq I (c), I (c) + 1 - i, i)))$
10		ballotth.r	$⊢ R = (c \in (O ∖ E) ⟼ S (c) [c])$
11		simpl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to C \in (O ∖ E)$
12	1 2 3 4 5 6 7 8 9	ballotlemsf1o	$⊢ C \in (O ∖ E) \to (S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \land {S (C)}^{-1} = S (C))$
13	12	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
14		f1ofun	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to Fun S (C)$
15	11 13 14	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to Fun S (C)$
16		simpr	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to J \in (1 \dots M + N)$
17		f1odm	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to dom S (C) = (1 \dots M + N)$
18	11 13 17	3syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to dom S (C) = (1 \dots M + N)$
19	16 18	eleqtrrd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to J \in dom S (C)$
20		fvimacnv	$⊢ (Fun S (C) \land J \in dom S (C)) \to (S (C) (J) \in C \leftrightarrow J \in {S (C)}^{-1} [C])$
21	15 19 20	syl2anc	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to (S (C) (J) \in C \leftrightarrow J \in {S (C)}^{-1} [C])$
22	1 2 3 4 5 6 7 8 9	ballotlemsv	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to S (C) (J) = if (J \leq I (C), I (C) + 1 - J, J)$
23	22	eleq1d	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to (S (C) (J) \in C \leftrightarrow if (J \leq I (C), I (C) + 1 - J, J) \in C)$
24	12	simprd	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} = S (C)$
25	24	imaeq1d	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} [C] = S (C) [C]$
26	1 2 3 4 5 6 7 8 9 10	ballotlemrval	$⊢ C \in (O ∖ E) \to R (C) = S (C) [C]$
27	25 26	eqtr4d	$⊢ C \in (O ∖ E) \to {S (C)}^{-1} [C] = R (C)$
28	27	eleq2d	$⊢ C \in (O ∖ E) \to (J \in {S (C)}^{-1} [C] \leftrightarrow J \in R (C))$
29	11 28	syl	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to (J \in {S (C)}^{-1} [C] \leftrightarrow J \in R (C))$
30	21 23 29	3bitr3rd	$⊢ (C \in (O ∖ E) \land J \in (1 \dots M + N)) \to (J \in R (C) \leftrightarrow if (J \leq I (C), I (C) + 1 - J, J) \in C)$

Metamath Proof Explorer

Theorem ballotlemrv

Proof