ballotlemirc

Description: Applying R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017) (Revised by AV, 6-Oct-2020)

	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) ⟼ inf (\{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	ballotlemirc	$⊢ C \in (O ∖ E) \to I (R (C)) = I (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) ⟼ inf (\{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	1 2 3 4 5 6 7 8 9 10	ballotlemrc	$⊢ C \in (O ∖ E) \to R (C) \in (O ∖ E)$
12	1 2 3 4 5 6 7 8	ballotlemi	$⊢ R (C) \in (O ∖ E) \to I (R (C)) = inf (\{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} ℝ <)$
13	11 12	syl	$⊢ C \in (O ∖ E) \to I (R (C)) = inf (\{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} ℝ <)$
14		ltso	$⊢ < Or ℝ$
15	14	a1i	$⊢ C \in (O ∖ E) \to < Or ℝ$
16	1 2 3 4 5 6 7 8	ballotlemiex	$⊢ C \in (O ∖ E) \to (I (C) \in (1 \dots M + N) \land F (C) (I (C)) = 0)$
17	16	simpld	$⊢ C \in (O ∖ E) \to I (C) \in (1 \dots M + N)$
18	17	elfzelzd	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
19	18	zred	$⊢ C \in (O ∖ E) \to I (C) \in ℝ$
20		eqid	$⊢ (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|) = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
21	1 2 3 4 5 6 7 8 9 10 20	ballotlemfrci	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = 0$
22		fveqeq2	$⊢ k = I (C) \to (F (R (C)) (k) = 0 \leftrightarrow F (R (C)) (I (C)) = 0)$
23	22	elrab	$⊢ I (C) \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \leftrightarrow (I (C) \in (1 \dots M + N) \land F (R (C)) (I (C)) = 0)$
24	17 21 23	sylanbrc	$⊢ C \in (O ∖ E) \to I (C) \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}$
25		elrabi	$⊢ y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \to y \in (1 \dots M + N)$
26	25	anim2i	$⊢ (C \in (O ∖ E) \land y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}) \to (C \in (O ∖ E) \land y \in (1 \dots M + N))$
27		simpr	$⊢ ((C \in (O ∖ E) \land y \in (1 \dots M + N)) \land y < I (C)) \to y < I (C)$
28	1 2 3 4 5 6 7 8 9 10	ballotlemfrcn0	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N) \land y < I (C)) \to F (R (C)) (y) \neq 0$
29	28	neneqd	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N) \land y < I (C)) \to \neg F (R (C)) (y) = 0$
30		fveqeq2	$⊢ k = y \to (F (R (C)) (k) = 0 \leftrightarrow F (R (C)) (y) = 0)$
31	30	elrab	$⊢ y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \leftrightarrow (y \in (1 \dots M + N) \land F (R (C)) (y) = 0)$
32	31	simprbi	$⊢ y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \to F (R (C)) (y) = 0$
33	29 32	nsyl	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N) \land y < I (C)) \to \neg y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}$
34	33	3expa	$⊢ ((C \in (O ∖ E) \land y \in (1 \dots M + N)) \land y < I (C)) \to \neg y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}$
35	27 34	syldan	$⊢ ((C \in (O ∖ E) \land y \in (1 \dots M + N)) \land y < I (C)) \to \neg y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}$
36	35	ex	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N)) \to (y < I (C) \to \neg y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\})$
37	36	con2d	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N)) \to (y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \to \neg y < I (C))$
38	37	imp	$⊢ ((C \in (O ∖ E) \land y \in (1 \dots M + N)) \land y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}) \to \neg y < I (C)$
39	26 38	sylancom	$⊢ (C \in (O ∖ E) \land y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}) \to \neg y < I (C)$
40	15 19 24 39	infmin	$⊢ C \in (O ∖ E) \to inf (\{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} ℝ <) = I (C)$
41	13 40	eqtrd	$⊢ C \in (O ∖ E) \to I (R (C)) = I (C)$

Metamath Proof Explorer

Theorem ballotlemirc

Proof