ballotlemro

Description: Range of R is included in O . (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	ballotlemro	$⊢ C \in (O ∖ E) \to R (C) \in O$

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	ballotlemrval	$⊢ C \in (O ∖ E) \to R (C) = S (C) [C]$
12		imassrn	$⊢ S (C) [C] \subseteq ran S (C)$
13	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))$
14	13	simpld	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N)$
15		f1ofo	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to S (C) : (1 \dots M + N) \underset{onto}{⟶} (1 \dots M + N)$
16		forn	$⊢ S (C) : (1 \dots M + N) \underset{onto}{⟶} (1 \dots M + N) \to ran S (C) = (1 \dots M + N)$
17	14 15 16	3syl	$⊢ C \in (O ∖ E) \to ran S (C) = (1 \dots M + N)$
18	12 17	sseqtrid	$⊢ C \in (O ∖ E) \to S (C) [C] \subseteq (1 \dots M + N)$
19	11 18	eqsstrd	$⊢ C \in (O ∖ E) \to R (C) \subseteq (1 \dots M + N)$
20		f1of1	$⊢ S (C) : (1 \dots M + N) \underset{1-1 onto}{⟶} (1 \dots M + N) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
21	14 20	syl	$⊢ C \in (O ∖ E) \to S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N)$
22		eldifi	$⊢ C \in (O ∖ E) \to C \in O$
23	1 2 3	ballotlemelo	$⊢ C \in O \leftrightarrow (C \subseteq (1 \dots M + N) \land \|C\| = M)$
24	22 23	sylib	$⊢ C \in (O ∖ E) \to (C \subseteq (1 \dots M + N) \land \|C\| = M)$
25	24	simpld	$⊢ C \in (O ∖ E) \to C \subseteq (1 \dots M + N)$
26		id	$⊢ C \in (O ∖ E) \to C \in (O ∖ E)$
27		f1imaeng	$⊢ (S (C) : (1 \dots M + N) \underset{1-1}{⟶} (1 \dots M + N) \land C \subseteq (1 \dots M + N) \land C \in (O ∖ E)) \to S (C) [C] \approx C$
28	21 25 26 27	syl3anc	$⊢ C \in (O ∖ E) \to S (C) [C] \approx C$
29	11 28	eqbrtrd	$⊢ C \in (O ∖ E) \to R (C) \approx C$
30		hasheni	$⊢ R (C) \approx C \to \|R (C)\| = \|C\|$
31	29 30	syl	$⊢ C \in (O ∖ E) \to \|R (C)\| = \|C\|$
32	24	simprd	$⊢ C \in (O ∖ E) \to \|C\| = M$
33	31 32	eqtrd	$⊢ C \in (O ∖ E) \to \|R (C)\| = M$
34	1 2 3	ballotlemelo	$⊢ R (C) \in O \leftrightarrow (R (C) \subseteq (1 \dots M + N) \land \|R (C)\| = M)$
35	19 33 34	sylanbrc	$⊢ C \in (O ∖ E) \to R (C) \in O$

Metamath Proof Explorer

Theorem ballotlemro

Proof