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 ⟼ x O
ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
ballotth.mgtn ⊢ N < M
ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
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 ⟼ x O
5 ballotth.f ⊢ F = c ∈ O ⟼ i ∈ ℤ ⟼ 1 … i ∩ c − 1 … i ∖ c
6 ballotth.e ⊢ E = c ∈ O | ∀ i ∈ 1 … M + N 0 < F ⁡ c ⁡ i
7 ballotth.mgtn ⊢ N < M
8 ballotth.i ⊢ I = c ∈ O ∖ E ⟼ sup k ∈ 1 … M + N | F ⁡ c ⁡ k = 0 ℝ <
9 ballotth.s ⊢ S = c ∈ O ∖ E ⟼ i ∈ 1 … M + N ⟼ if i ≤ I ⁡ c I ⁡ c + 1 - i i
10 ballotth.r ⊢ R = c ∈ O ∖ E ⟼ S ⁡ c c
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