ballotlemrval

	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	ballotlemrval	$⊢ C \in (O ∖ E) \to R (C) = S (C) [C]$

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		fveq2	$⊢ d = C \to S (d) = S (C)$
12		id	$⊢ d = C \to d = C$
13	11 12	imaeq12d	$⊢ d = C \to S (d) [d] = S (C) [C]$
14		fveq2	$⊢ c = d \to S (c) = S (d)$
15		id	$⊢ c = d \to c = d$
16	14 15	imaeq12d	$⊢ c = d \to S (c) [c] = S (d) [d]$
17	16	cbvmptv	$⊢ (c \in (O ∖ E) ⟼ S (c) [c]) = (d \in (O ∖ E) ⟼ S (d) [d])$
18	10 17	eqtri	$⊢ R = (d \in (O ∖ E) ⟼ S (d) [d])$
19		fvex	$⊢ S (C) \in V$
20		imaexg	$⊢ S (C) \in V \to S (C) [C] \in V$
21	19 20	ax-mp	$⊢ S (C) [C] \in V$
22	13 18 21	fvmpt	$⊢ C \in (O ∖ E) \to R (C) = S (C) [C]$

Metamath Proof Explorer