Metamath Proof Explorer

Theorem ballotlemgun

Description: A property of the defined .^ operator. (Contributed by Thierry Arnoux, 26-Apr-2017)

Ref Expression
Hypotheses ballotth.m ⊢M∈ℕ
ballotth.n ⊢N∈ℕ
ballotth.o ⊢O=c∈𝒫1…M+N|c=M
ballotth.p ⊢P=x∈𝒫O⟼xO
ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
ballotth.mgtn ⊢N<M
ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
ballotth.r ⊢R=c∈O∖E⟼S⁡cc
ballotlemg ⊢×˙=u∈Fin,v∈Fin⟼v∩u−v∖u
ballotlemgun.1 ⊢φ→U∈Fin
ballotlemgun.2 ⊢φ→V∈Fin
ballotlemgun.3 ⊢φ→W∈Fin
ballotlemgun.4 ⊢φ→V∩W=∅
Assertion ballotlemgun ⊢φ→U×˙V∪W=U×˙V+U×˙W

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢M∈ℕ
2 ballotth.n ⊢N∈ℕ
3 ballotth.o ⊢O=c∈𝒫1…M+N|c=M
4 ballotth.p ⊢P=x∈𝒫O⟼xO
5 ballotth.f ⊢F=c∈O⟼i∈ℤ⟼1…i∩c−1…i∖c
6 ballotth.e ⊢E=c∈O|∀i∈1…M+N0<F⁡c⁡i
7 ballotth.mgtn ⊢N<M
8 ballotth.i ⊢I=c∈O∖E⟼supk∈1…M+N|F⁡c⁡k=0ℝ<
9 ballotth.s ⊢S=c∈O∖E⟼i∈1…M+N⟼ifi≤I⁡cI⁡c+1-ii
10 ballotth.r ⊢R=c∈O∖E⟼S⁡cc
11 ballotlemg ⊢×˙=u∈Fin,v∈Fin⟼v∩u−v∖u
12 ballotlemgun.1 ⊢φ→U∈Fin
13 ballotlemgun.2 ⊢φ→V∈Fin
14 ballotlemgun.3 ⊢φ→W∈Fin
15 ballotlemgun.4 ⊢φ→V∩W=∅
16 indir ⊢V∪W∩U=V∩U∪W∩U
17 16 fveq2i ⊢V∪W∩U=V∩U∪W∩U
18 infi ⊢V∈Fin→V∩U∈Fin
19 13 18 syl ⊢φ→V∩U∈Fin
20 infi ⊢W∈Fin→W∩U∈Fin
21 14 20 syl ⊢φ→W∩U∈Fin
22 15 ineq1d ⊢φ→V∩W∩U=∅∩U
23 inindir ⊢V∩W∩U=V∩U∩W∩U
24 0in ⊢∅∩U=∅
25 22 23 24 3eqtr3g ⊢φ→V∩U∩W∩U=∅
26 hashun ⊢V∩U∈Fin∧W∩U∈Fin∧V∩U∩W∩U=∅→V∩U∪W∩U=V∩U+W∩U
27 19 21 25 26 syl3anc ⊢φ→V∩U∪W∩U=V∩U+W∩U
28 17 27 eqtrid ⊢φ→V∪W∩U=V∩U+W∩U
29 difundir ⊢V∪W∖U=V∖U∪W∖U
30 29 fveq2i ⊢V∪W∖U=V∖U∪W∖U
31 diffi ⊢V∈Fin→V∖U∈Fin
32 13 31 syl ⊢φ→V∖U∈Fin
33 diffi ⊢W∈Fin→W∖U∈Fin
34 14 33 syl ⊢φ→W∖U∈Fin
35 15 difeq1d ⊢φ→V∩W∖U=∅∖U
36 difindir ⊢V∩W∖U=V∖U∩W∖U
37 0dif ⊢∅∖U=∅
38 35 36 37 3eqtr3g ⊢φ→V∖U∩W∖U=∅
39 hashun ⊢V∖U∈Fin∧W∖U∈Fin∧V∖U∩W∖U=∅→V∖U∪W∖U=V∖U+W∖U
40 32 34 38 39 syl3anc ⊢φ→V∖U∪W∖U=V∖U+W∖U
41 30 40 eqtrid ⊢φ→V∪W∖U=V∖U+W∖U
42 28 41 oveq12d ⊢φ→V∪W∩U−V∪W∖U=V∩U+W∩U-V∖U+W∖U
43 hashcl ⊢V∩U∈Fin→V∩U∈ℕ0
44 13 18 43 3syl ⊢φ→V∩U∈ℕ0
45 44 nn0cnd ⊢φ→V∩U∈ℂ
46 hashcl ⊢W∩U∈Fin→W∩U∈ℕ0
47 14 20 46 3syl ⊢φ→W∩U∈ℕ0
48 47 nn0cnd ⊢φ→W∩U∈ℂ
49 hashcl ⊢V∖U∈Fin→V∖U∈ℕ0
50 13 31 49 3syl ⊢φ→V∖U∈ℕ0
51 50 nn0cnd ⊢φ→V∖U∈ℂ
52 hashcl ⊢W∖U∈Fin→W∖U∈ℕ0
53 14 33 52 3syl ⊢φ→W∖U∈ℕ0
54 53 nn0cnd ⊢φ→W∖U∈ℂ
55 45 48 51 54 addsub4d ⊢φ→V∩U+W∩U-V∖U+W∖U=V∩U−V∖U+W∩U-W∖U
56 42 55 eqtrd ⊢φ→V∪W∩U−V∪W∖U=V∩U−V∖U+W∩U-W∖U
57 unfi ⊢V∈Fin∧W∈Fin→V∪W∈Fin
58 13 14 57 syl2anc ⊢φ→V∪W∈Fin
59 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢U∈Fin∧V∪W∈Fin→U×˙V∪W=V∪W∩U−V∪W∖U
60 12 58 59 syl2anc ⊢φ→U×˙V∪W=V∪W∩U−V∪W∖U
61 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢U∈Fin∧V∈Fin→U×˙V=V∩U−V∖U
62 12 13 61 syl2anc ⊢φ→U×˙V=V∩U−V∖U
63 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢U∈Fin∧W∈Fin→U×˙W=W∩U−W∖U
64 12 14 63 syl2anc ⊢φ→U×˙W=W∩U−W∖U
65 62 64 oveq12d ⊢φ→U×˙V+U×˙W=V∩U−V∖U+W∩U-W∖U
66 56 60 65 3eqtr4d ⊢φ→U×˙V∪W=U×˙V+U×˙W