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) ⟼ 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	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) ⟼ 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	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)) = sup (\{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} ℝ <)$
13	11 12	syl	$⊢ C \in (O ∖ E) \to I (R (C)) = sup (\{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		elfzelz	$⊢ I (C) \in (1 \dots M + N) \to I (C) \in ℤ$
19	17 18	syl	$⊢ C \in (O ∖ E) \to I (C) \in ℤ$
20	19	zred	$⊢ C \in (O ∖ E) \to I (C) \in ℝ$
21		eqid	$⊢ (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|) = (u \in Fin, v \in Fin ⟼ \|v \cap u\| - \|v ∖ u\|)$
22	1 2 3 4 5 6 7 8 9 10 21	ballotlemfrci	$⊢ C \in (O ∖ E) \to F (R (C)) (I (C)) = 0$
23		fveqeq2	$⊢ k = I (C) \to (F (R (C)) (k) = 0 \leftrightarrow F (R (C)) (I (C)) = 0)$
24	23	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)$
25	17 22 24	sylanbrc	$⊢ C \in (O ∖ E) \to I (C) \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}$
26		elrabi	$⊢ y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \to y \in (1 \dots M + N)$
27	26	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))$
28		simpr	$⊢ ((C \in (O ∖ E) \land y \in (1 \dots M + N)) \land y < I (C)) \to y < I (C)$
29	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$
30	29	neneqd	$⊢ (C \in (O ∖ E) \land y \in (1 \dots M + N) \land y < I (C)) \to \neg F (R (C)) (y) = 0$
31		fveqeq2	$⊢ k = y \to (F (R (C)) (k) = 0 \leftrightarrow F (R (C)) (y) = 0)$
32	31	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)$
33	32	simprbi	$⊢ y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} \to F (R (C)) (y) = 0$
34	30 33	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\}$
35	34	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\}$
36	28 35	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\}$
37	36	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\})$
38	37	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))$
39	38	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)$
40	27 39	sylancom	$⊢ (C \in (O ∖ E) \land y \in \{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\}) \to \neg y < I (C)$
41	15 20 25 40	infmin	$⊢ C \in (O ∖ E) \to sup (\{k \in (1 \dots M + N) \| F (R (C)) (k) = 0\} ℝ <) = I (C)$
42	13 41	eqtrd	$⊢ C \in (O ∖ E) \to I (R (C)) = I (C)$

Metamath Proof Explorer

Theorem ballotlemirc

Proof