# Metamath Proof Explorer

## Theorem 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}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
ballotth.e ${⊢}{E}=\left\{{c}\in {O}|\forall {i}\in \left(1\dots {M}+{N}\right)\phantom{\rule{.4em}{0ex}}0<{F}\left({c}\right)\left({i}\right)\right\}$
ballotth.mgtn ${⊢}{N}<{M}$
ballotth.i ${⊢}{I}=\left({c}\in \left({O}\setminus {E}\right)⟼sup\left(\left\{{k}\in \left(1\dots {M}+{N}\right)|{F}\left({c}\right)\left({k}\right)=0\right\},ℝ,<\right)\right)$
ballotth.s ${⊢}{S}=\left({c}\in \left({O}\setminus {E}\right)⟼\left({i}\in \left(1\dots {M}+{N}\right)⟼if\left({i}\le {I}\left({c}\right),{I}\left({c}\right)+1-{i},{i}\right)\right)\right)$
ballotth.r ${⊢}{R}=\left({c}\in \left({O}\setminus {E}\right)⟼{S}\left({c}\right)\left[{c}\right]\right)$
Assertion ballotlemro ${⊢}{C}\in \left({O}\setminus {E}\right)\to {R}\left({C}\right)\in {O}$

### Proof

Step Hyp Ref Expression
1 ballotth.m ${⊢}{M}\in ℕ$
2 ballotth.n ${⊢}{N}\in ℕ$
3 ballotth.o ${⊢}{O}=\left\{{c}\in 𝒫\left(1\dots {M}+{N}\right)|\left|{c}\right|={M}\right\}$
4 ballotth.p ${⊢}{P}=\left({x}\in 𝒫{O}⟼\frac{\left|{x}\right|}{\left|{O}\right|}\right)$
5 ballotth.f ${⊢}{F}=\left({c}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)\right)$
6 ballotth.e ${⊢}{E}=\left\{{c}\in {O}|\forall {i}\in \left(1\dots {M}+{N}\right)\phantom{\rule{.4em}{0ex}}0<{F}\left({c}\right)\left({i}\right)\right\}$
7 ballotth.mgtn ${⊢}{N}<{M}$
8 ballotth.i ${⊢}{I}=\left({c}\in \left({O}\setminus {E}\right)⟼sup\left(\left\{{k}\in \left(1\dots {M}+{N}\right)|{F}\left({c}\right)\left({k}\right)=0\right\},ℝ,<\right)\right)$
9 ballotth.s ${⊢}{S}=\left({c}\in \left({O}\setminus {E}\right)⟼\left({i}\in \left(1\dots {M}+{N}\right)⟼if\left({i}\le {I}\left({c}\right),{I}\left({c}\right)+1-{i},{i}\right)\right)\right)$
10 ballotth.r ${⊢}{R}=\left({c}\in \left({O}\setminus {E}\right)⟼{S}\left({c}\right)\left[{c}\right]\right)$
11 1 2 3 4 5 6 7 8 9 10 ballotlemrval ${⊢}{C}\in \left({O}\setminus {E}\right)\to {R}\left({C}\right)={S}\left({C}\right)\left[{C}\right]$
12 imassrn ${⊢}{S}\left({C}\right)\left[{C}\right]\subseteq \mathrm{ran}{S}\left({C}\right)$
13 1 2 3 4 5 6 7 8 9 ballotlemsf1o ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left({S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\wedge {{S}\left({C}\right)}^{-1}={S}\left({C}\right)\right)$
14 13 simpld ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)$
15 f1ofo ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{onto}{⟶}\left(1\dots {M}+{N}\right)$
16 forn ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{onto}{⟶}\left(1\dots {M}+{N}\right)\to \mathrm{ran}{S}\left({C}\right)=\left(1\dots {M}+{N}\right)$
17 14 15 16 3syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to \mathrm{ran}{S}\left({C}\right)=\left(1\dots {M}+{N}\right)$
18 12 17 sseqtrid ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right)\left[{C}\right]\subseteq \left(1\dots {M}+{N}\right)$
19 11 18 eqsstrd ${⊢}{C}\in \left({O}\setminus {E}\right)\to {R}\left({C}\right)\subseteq \left(1\dots {M}+{N}\right)$
20 f1of1 ${⊢}{S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1 onto}{⟶}\left(1\dots {M}+{N}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1}{⟶}\left(1\dots {M}+{N}\right)$
21 14 20 syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1}{⟶}\left(1\dots {M}+{N}\right)$
22 eldifi ${⊢}{C}\in \left({O}\setminus {E}\right)\to {C}\in {O}$
23 1 2 3 ballotlemelo ${⊢}{C}\in {O}↔\left({C}\subseteq \left(1\dots {M}+{N}\right)\wedge \left|{C}\right|={M}\right)$
24 22 23 sylib ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left({C}\subseteq \left(1\dots {M}+{N}\right)\wedge \left|{C}\right|={M}\right)$
25 24 simpld ${⊢}{C}\in \left({O}\setminus {E}\right)\to {C}\subseteq \left(1\dots {M}+{N}\right)$
26 id ${⊢}{C}\in \left({O}\setminus {E}\right)\to {C}\in \left({O}\setminus {E}\right)$
27 f1imaeng ${⊢}\left({S}\left({C}\right):\left(1\dots {M}+{N}\right)\underset{1-1}{⟶}\left(1\dots {M}+{N}\right)\wedge {C}\subseteq \left(1\dots {M}+{N}\right)\wedge {C}\in \left({O}\setminus {E}\right)\right)\to {S}\left({C}\right)\left[{C}\right]\approx {C}$
28 21 25 26 27 syl3anc ${⊢}{C}\in \left({O}\setminus {E}\right)\to {S}\left({C}\right)\left[{C}\right]\approx {C}$
29 11 28 eqbrtrd ${⊢}{C}\in \left({O}\setminus {E}\right)\to {R}\left({C}\right)\approx {C}$
30 hasheni ${⊢}{R}\left({C}\right)\approx {C}\to \left|{R}\left({C}\right)\right|=\left|{C}\right|$
31 29 30 syl ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left|{R}\left({C}\right)\right|=\left|{C}\right|$
32 24 simprd ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left|{C}\right|={M}$
33 31 32 eqtrd ${⊢}{C}\in \left({O}\setminus {E}\right)\to \left|{R}\left({C}\right)\right|={M}$
34 1 2 3 ballotlemelo ${⊢}{R}\left({C}\right)\in {O}↔\left({R}\left({C}\right)\subseteq \left(1\dots {M}+{N}\right)\wedge \left|{R}\left({C}\right)\right|={M}\right)$
35 19 33 34 sylanbrc ${⊢}{C}\in \left({O}\setminus {E}\right)\to {R}\left({C}\right)\in {O}$