# Metamath Proof Explorer

## Theorem ballotlemgval

Description: Expand the value of .^ . (Contributed by Thierry Arnoux, 21-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)$
ballotlemg
Assertion ballotlemgval

### 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 ballotlemg
12 ineq2 ${⊢}{u}={U}\to {v}\cap {u}={v}\cap {U}$
13 12 fveq2d ${⊢}{u}={U}\to \left|{v}\cap {u}\right|=\left|{v}\cap {U}\right|$
14 difeq2 ${⊢}{u}={U}\to {v}\setminus {u}={v}\setminus {U}$
15 14 fveq2d ${⊢}{u}={U}\to \left|{v}\setminus {u}\right|=\left|{v}\setminus {U}\right|$
16 13 15 oveq12d ${⊢}{u}={U}\to \left|{v}\cap {u}\right|-\left|{v}\setminus {u}\right|=\left|{v}\cap {U}\right|-\left|{v}\setminus {U}\right|$
17 ineq1 ${⊢}{v}={V}\to {v}\cap {U}={V}\cap {U}$
18 17 fveq2d ${⊢}{v}={V}\to \left|{v}\cap {U}\right|=\left|{V}\cap {U}\right|$
19 difeq1 ${⊢}{v}={V}\to {v}\setminus {U}={V}\setminus {U}$
20 19 fveq2d ${⊢}{v}={V}\to \left|{v}\setminus {U}\right|=\left|{V}\setminus {U}\right|$
21 18 20 oveq12d ${⊢}{v}={V}\to \left|{v}\cap {U}\right|-\left|{v}\setminus {U}\right|=\left|{V}\cap {U}\right|-\left|{V}\setminus {U}\right|$
22 ovex ${⊢}\left|{V}\cap {U}\right|-\left|{V}\setminus {U}\right|\in \mathrm{V}$
23 16 21 11 22 ovmpo