# Metamath Proof Explorer

## Theorem ballotlemfval

Description: The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016)

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)$
ballotlemfval.c ${⊢}{\phi }\to {C}\in {O}$
ballotlemfval.j ${⊢}{\phi }\to {J}\in ℤ$
Assertion ballotlemfval ${⊢}{\phi }\to {F}\left({C}\right)\left({J}\right)=\left|\left(1\dots {J}\right)\cap {C}\right|-\left|\left(1\dots {J}\right)\setminus {C}\right|$

### 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 ballotlemfval.c ${⊢}{\phi }\to {C}\in {O}$
7 ballotlemfval.j ${⊢}{\phi }\to {J}\in ℤ$
8 simpl ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to {b}={C}$
9 8 ineq2d ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to \left(1\dots {i}\right)\cap {b}=\left(1\dots {i}\right)\cap {C}$
10 9 fveq2d ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to \left|\left(1\dots {i}\right)\cap {b}\right|=\left|\left(1\dots {i}\right)\cap {C}\right|$
11 8 difeq2d ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to \left(1\dots {i}\right)\setminus {b}=\left(1\dots {i}\right)\setminus {C}$
12 11 fveq2d ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to \left|\left(1\dots {i}\right)\setminus {b}\right|=\left|\left(1\dots {i}\right)\setminus {C}\right|$
13 10 12 oveq12d ${⊢}\left({b}={C}\wedge {i}\in ℤ\right)\to \left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|=\left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|$
14 13 mpteq2dva ${⊢}{b}={C}\to \left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|\right)=\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|\right)$
15 ineq2 ${⊢}{b}={c}\to \left(1\dots {i}\right)\cap {b}=\left(1\dots {i}\right)\cap {c}$
16 15 fveq2d ${⊢}{b}={c}\to \left|\left(1\dots {i}\right)\cap {b}\right|=\left|\left(1\dots {i}\right)\cap {c}\right|$
17 difeq2 ${⊢}{b}={c}\to \left(1\dots {i}\right)\setminus {b}=\left(1\dots {i}\right)\setminus {c}$
18 17 fveq2d ${⊢}{b}={c}\to \left|\left(1\dots {i}\right)\setminus {b}\right|=\left|\left(1\dots {i}\right)\setminus {c}\right|$
19 16 18 oveq12d ${⊢}{b}={c}\to \left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|=\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|$
20 19 mpteq2dv ${⊢}{b}={c}\to \left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|\right)=\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {c}\right|-\left|\left(1\dots {i}\right)\setminus {c}\right|\right)$
21 20 cbvmptv ${⊢}\left({b}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|\right)\right)=\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)$
22 5 21 eqtr4i ${⊢}{F}=\left({b}\in {O}⟼\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {b}\right|-\left|\left(1\dots {i}\right)\setminus {b}\right|\right)\right)$
23 zex ${⊢}ℤ\in \mathrm{V}$
24 23 mptex ${⊢}\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|\right)\in \mathrm{V}$
25 14 22 24 fvmpt ${⊢}{C}\in {O}\to {F}\left({C}\right)=\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|\right)$
26 6 25 syl ${⊢}{\phi }\to {F}\left({C}\right)=\left({i}\in ℤ⟼\left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|\right)$
27 oveq2 ${⊢}{i}={J}\to \left(1\dots {i}\right)=\left(1\dots {J}\right)$
28 27 ineq1d ${⊢}{i}={J}\to \left(1\dots {i}\right)\cap {C}=\left(1\dots {J}\right)\cap {C}$
29 28 fveq2d ${⊢}{i}={J}\to \left|\left(1\dots {i}\right)\cap {C}\right|=\left|\left(1\dots {J}\right)\cap {C}\right|$
30 27 difeq1d ${⊢}{i}={J}\to \left(1\dots {i}\right)\setminus {C}=\left(1\dots {J}\right)\setminus {C}$
31 30 fveq2d ${⊢}{i}={J}\to \left|\left(1\dots {i}\right)\setminus {C}\right|=\left|\left(1\dots {J}\right)\setminus {C}\right|$
32 29 31 oveq12d ${⊢}{i}={J}\to \left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|=\left|\left(1\dots {J}\right)\cap {C}\right|-\left|\left(1\dots {J}\right)\setminus {C}\right|$
33 32 adantl ${⊢}\left({\phi }\wedge {i}={J}\right)\to \left|\left(1\dots {i}\right)\cap {C}\right|-\left|\left(1\dots {i}\right)\setminus {C}\right|=\left|\left(1\dots {J}\right)\cap {C}\right|-\left|\left(1\dots {J}\right)\setminus {C}\right|$
34 ovexd ${⊢}{\phi }\to \left|\left(1\dots {J}\right)\cap {C}\right|-\left|\left(1\dots {J}\right)\setminus {C}\right|\in \mathrm{V}$
35 26 33 7 34 fvmptd ${⊢}{\phi }\to {F}\left({C}\right)\left({J}\right)=\left|\left(1\dots {J}\right)\cap {C}\right|-\left|\left(1\dots {J}\right)\setminus {C}\right|$