Theorem ballotlemgval

Description: Expand the value of .^ . (Contributed by Thierry Arnoux, 21-Apr-2017)

	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)$$
	ballotth.e	$$⊢E=\left\{c\in O|\forall i\in \left(1\dots M+N\right)0<F\left(c\right)\left(i\right)\right\}$$
	ballotth.mgtn	$$⊢N<M$$
	ballotth.i	$$⊢I=\left(c\in \left(O\setminus E\right)⟼inf\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	$$⊢\underset{\dot{}}{\times }=\left(u\in \mathrm{Fin},v\in \mathrm{Fin}⟼\left|v\cap u\right|-\left|v\setminus u\right|\right)$$
Assertion	ballotlemgval	$$⊢\left(U\in \mathrm{Fin}\wedge V\in \mathrm{Fin}\right)\to U\underset{\dot{}}{\times }V=\left|V\cap U\right|-\left|V\setminus U\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		ballotth.e	$$⊢E=\left\{c\in O|\forall i\in \left(1\dots M+N\right)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)⟼inf\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	$$⊢\underset{\dot{}}{\times }=\left(u\in \mathrm{Fin},v\in \mathrm{Fin}⟼\left|v\cap u\right|-\left|v\setminus u\right|\right)$$
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	$$⊢\left(U\in \mathrm{Fin}\wedge V\in \mathrm{Fin}\right)\to U\underset{\dot{}}{\times }V=\left|V\cap U\right|-\left|V\setminus U\right|$$