Theorem ballotlemfval

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

	Ref	Expression
Hypotheses	ballotth.m	$$⊢M\in \mathbb{N}$$
	ballotth.n	$$⊢N\in \mathbb{N}$$
	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 \mathbb{Z}⟼\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 \mathbb{Z}$$
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 \mathbb{N}$$
2		ballotth.n	$$⊢N\in \mathbb{N}$$
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 \mathbb{Z}⟼\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 \mathbb{Z}$$
8		simpl	$$⊢\left(b=C\wedge i\in \mathbb{Z}\right)\to b=C$$
9	8	ineq2d	$$⊢\left(b=C\wedge i\in \mathbb{Z}\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 \mathbb{Z}\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 \mathbb{Z}\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 \mathbb{Z}\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 \mathbb{Z}\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 \mathbb{Z}⟼\left|\left(1\dots i\right)\cap b\right|-\left|\left(1\dots i\right)\setminus b\right|\right)=\left(i\in \mathbb{Z}⟼\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 \mathbb{Z}⟼\left|\left(1\dots i\right)\cap b\right|-\left|\left(1\dots i\right)\setminus b\right|\right)=\left(i\in \mathbb{Z}⟼\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 \mathbb{Z}⟼\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 \mathbb{Z}⟼\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 \mathbb{Z}⟼\left|\left(1\dots i\right)\cap b\right|-\left|\left(1\dots i\right)\setminus b\right|\right)\right)$$
23		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
24	23	mptex	$$⊢\left(i\in \mathbb{Z}⟼\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 \mathbb{Z}⟼\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 \mathbb{Z}⟼\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|$$