Metamath Proof Explorer

Theorem ballotlemgun

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

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
ballotth.mgtn ⊢ 𝑁 < 𝑀
ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
ballotlemgun.1 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
ballotlemgun.2 ⊢ ( 𝜑 → 𝑉 ∈ Fin )
ballotlemgun.3 ⊢ ( 𝜑 → 𝑊 ∈ Fin )
ballotlemgun.4 ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑊 ) = ∅ )
Assertion ballotlemgun ( 𝜑 → ( 𝑈 ↑ ( 𝑉 ∪ 𝑊 ) ) = ( ( 𝑈 ↑ 𝑉 ) + ( 𝑈 ↑ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotth.e ⊢ 𝐸 = { 𝑐 ∈ 𝑂 ∣ ∀ 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) 0 < ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑖 ) }
7 ballotth.mgtn ⊢ 𝑁 < 𝑀
8 ballotth.i ⊢ 𝐼 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ inf ( { 𝑘 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ( 𝐹 ‘ 𝑐 ) ‘ 𝑘 ) = 0 } , ℝ , < ) )
9 ballotth.s ⊢ 𝑆 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( 𝑖 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ↦ if ( 𝑖 ≤ ( 𝐼 ‘ 𝑐 ) , ( ( ( 𝐼 ‘ 𝑐 ) + 1 ) − 𝑖 ) , 𝑖 ) ) )
10 ballotth.r ⊢ 𝑅 = ( 𝑐 ∈ ( 𝑂 ∖ 𝐸 ) ↦ ( ( 𝑆 ‘ 𝑐 ) “ 𝑐 ) )
11 ballotlemg ⊢ ↑ = ( 𝑢 ∈ Fin , 𝑣 ∈ Fin ↦ ( ( ♯ ‘ ( 𝑣 ∩ 𝑢 ) ) − ( ♯ ‘ ( 𝑣 ∖ 𝑢 ) ) ) )
12 ballotlemgun.1 ⊢ ( 𝜑 → 𝑈 ∈ Fin )
13 ballotlemgun.2 ⊢ ( 𝜑 → 𝑉 ∈ Fin )
14 ballotlemgun.3 ⊢ ( 𝜑 → 𝑊 ∈ Fin )
15 ballotlemgun.4 ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑊 ) = ∅ )
16 indir ⊢ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) = ( ( 𝑉 ∩ 𝑈 ) ∪ ( 𝑊 ∩ 𝑈 ) )
17 16 fveq2i ⊢ ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) = ( ♯ ‘ ( ( 𝑉 ∩ 𝑈 ) ∪ ( 𝑊 ∩ 𝑈 ) ) )
18 infi ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∩ 𝑈 ) ∈ Fin )
19 13 18 syl ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑈 ) ∈ Fin )
20 infi ⊢ ( 𝑊 ∈ Fin → ( 𝑊 ∩ 𝑈 ) ∈ Fin )
21 14 20 syl ⊢ ( 𝜑 → ( 𝑊 ∩ 𝑈 ) ∈ Fin )
22 15 ineq1d ⊢ ( 𝜑 → ( ( 𝑉 ∩ 𝑊 ) ∩ 𝑈 ) = ( ∅ ∩ 𝑈 ) )
23 inindir ⊢ ( ( 𝑉 ∩ 𝑊 ) ∩ 𝑈 ) = ( ( 𝑉 ∩ 𝑈 ) ∩ ( 𝑊 ∩ 𝑈 ) )
24 0in ⊢ ( ∅ ∩ 𝑈 ) = ∅
25 22 23 24 3eqtr3g ⊢ ( 𝜑 → ( ( 𝑉 ∩ 𝑈 ) ∩ ( 𝑊 ∩ 𝑈 ) ) = ∅ )
26 hashun ⊢ ( ( ( 𝑉 ∩ 𝑈 ) ∈ Fin ∧ ( 𝑊 ∩ 𝑈 ) ∈ Fin ∧ ( ( 𝑉 ∩ 𝑈 ) ∩ ( 𝑊 ∩ 𝑈 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝑉 ∩ 𝑈 ) ∪ ( 𝑊 ∩ 𝑈 ) ) ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ) )
27 19 21 25 26 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑉 ∩ 𝑈 ) ∪ ( 𝑊 ∩ 𝑈 ) ) ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ) )
28 17 27 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ) )
29 difundir ⊢ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) = ( ( 𝑉 ∖ 𝑈 ) ∪ ( 𝑊 ∖ 𝑈 ) )
30 29 fveq2i ⊢ ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) = ( ♯ ‘ ( ( 𝑉 ∖ 𝑈 ) ∪ ( 𝑊 ∖ 𝑈 ) ) )
31 diffi ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ 𝑈 ) ∈ Fin )
32 13 31 syl ⊢ ( 𝜑 → ( 𝑉 ∖ 𝑈 ) ∈ Fin )
33 diffi ⊢ ( 𝑊 ∈ Fin → ( 𝑊 ∖ 𝑈 ) ∈ Fin )
34 14 33 syl ⊢ ( 𝜑 → ( 𝑊 ∖ 𝑈 ) ∈ Fin )
35 15 difeq1d ⊢ ( 𝜑 → ( ( 𝑉 ∩ 𝑊 ) ∖ 𝑈 ) = ( ∅ ∖ 𝑈 ) )
36 difindir ⊢ ( ( 𝑉 ∩ 𝑊 ) ∖ 𝑈 ) = ( ( 𝑉 ∖ 𝑈 ) ∩ ( 𝑊 ∖ 𝑈 ) )
37 0dif ⊢ ( ∅ ∖ 𝑈 ) = ∅
38 35 36 37 3eqtr3g ⊢ ( 𝜑 → ( ( 𝑉 ∖ 𝑈 ) ∩ ( 𝑊 ∖ 𝑈 ) ) = ∅ )
39 hashun ⊢ ( ( ( 𝑉 ∖ 𝑈 ) ∈ Fin ∧ ( 𝑊 ∖ 𝑈 ) ∈ Fin ∧ ( ( 𝑉 ∖ 𝑈 ) ∩ ( 𝑊 ∖ 𝑈 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝑉 ∖ 𝑈 ) ∪ ( 𝑊 ∖ 𝑈 ) ) ) = ( ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) )
40 32 34 38 39 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑉 ∖ 𝑈 ) ∪ ( 𝑊 ∖ 𝑈 ) ) ) = ( ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) )
41 30 40 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) = ( ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) )
42 28 41 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) − ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) ) = ( ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ) − ( ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) ) )
43 hashcl ⊢ ( ( 𝑉 ∩ 𝑈 ) ∈ Fin → ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) ∈ ℕ0 )
44 13 18 43 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) ∈ ℕ0 )
45 44 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) ∈ ℂ )
46 hashcl ⊢ ( ( 𝑊 ∩ 𝑈 ) ∈ Fin → ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ∈ ℕ0 )
47 14 20 46 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ∈ ℕ0 )
48 47 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ∈ ℂ )
49 hashcl ⊢ ( ( 𝑉 ∖ 𝑈 ) ∈ Fin → ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ∈ ℕ0 )
50 13 31 49 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ∈ ℕ0 )
51 50 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ∈ ℂ )
52 hashcl ⊢ ( ( 𝑊 ∖ 𝑈 ) ∈ Fin → ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ∈ ℕ0 )
53 14 33 52 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ∈ ℕ0 )
54 53 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ∈ ℂ )
55 45 48 51 54 addsub4d ⊢ ( 𝜑 → ( ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) ) − ( ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) + ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) ) = ( ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) + ( ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) ) )
56 42 55 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) − ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) ) = ( ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) + ( ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) ) )
57 unfi ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑊 ∈ Fin ) → ( 𝑉 ∪ 𝑊 ) ∈ Fin )
58 13 14 57 syl2anc ⊢ ( 𝜑 → ( 𝑉 ∪ 𝑊 ) ∈ Fin )
59 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢ ( ( 𝑈 ∈ Fin ∧ ( 𝑉 ∪ 𝑊 ) ∈ Fin ) → ( 𝑈 ↑ ( 𝑉 ∪ 𝑊 ) ) = ( ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) − ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) ) )
60 12 58 59 syl2anc ⊢ ( 𝜑 → ( 𝑈 ↑ ( 𝑉 ∪ 𝑊 ) ) = ( ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∩ 𝑈 ) ) − ( ♯ ‘ ( ( 𝑉 ∪ 𝑊 ) ∖ 𝑈 ) ) ) )
61 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢ ( ( 𝑈 ∈ Fin ∧ 𝑉 ∈ Fin ) → ( 𝑈 ↑ 𝑉 ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) )
62 12 13 61 syl2anc ⊢ ( 𝜑 → ( 𝑈 ↑ 𝑉 ) = ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) )
63 1 2 3 4 5 6 7 8 9 10 11 ballotlemgval ⊢ ( ( 𝑈 ∈ Fin ∧ 𝑊 ∈ Fin ) → ( 𝑈 ↑ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) )
64 12 14 63 syl2anc ⊢ ( 𝜑 → ( 𝑈 ↑ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) )
65 62 64 oveq12d ⊢ ( 𝜑 → ( ( 𝑈 ↑ 𝑉 ) + ( 𝑈 ↑ 𝑊 ) ) = ( ( ( ♯ ‘ ( 𝑉 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑉 ∖ 𝑈 ) ) ) + ( ( ♯ ‘ ( 𝑊 ∩ 𝑈 ) ) − ( ♯ ‘ ( 𝑊 ∖ 𝑈 ) ) ) ) )
66 56 60 65 3eqtr4d ⊢ ( 𝜑 → ( 𝑈 ↑ ( 𝑉 ∪ 𝑊 ) ) = ( ( 𝑈 ↑ 𝑉 ) + ( 𝑈 ↑ 𝑊 ) ) )