Metamath Proof Explorer

Theorem ballotlemfval

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

Ref Expression
Hypotheses ballotth.m ⊢ 𝑀 ∈ ℕ
ballotth.n ⊢ 𝑁 ∈ ℕ
ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
ballotlemfval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
ballotlemfval.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
Assertion ballotlemfval ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m ⊢ 𝑀 ∈ ℕ
2 ballotth.n ⊢ 𝑁 ∈ ℕ
3 ballotth.o ⊢ 𝑂 = { 𝑐 ∈ 𝒫 ( 1 ... ( 𝑀 + 𝑁 ) ) ∣ ( ♯ ‘ 𝑐 ) = 𝑀 }
4 ballotth.p ⊢ 𝑃 = ( 𝑥 ∈ 𝒫 𝑂 ↦ ( ( ♯ ‘ 𝑥 ) / ( ♯ ‘ 𝑂 ) ) )
5 ballotth.f ⊢ 𝐹 = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
6 ballotlemfval.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑂 )
7 ballotlemfval.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
8 simpl ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → 𝑏 = 𝐶 )
9 8 ineq2d ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → ( ( 1 ... 𝑖 ) ∩ 𝑏 ) = ( ( 1 ... 𝑖 ) ∩ 𝐶 ) )
10 9 fveq2d ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) = ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) )
11 8 difeq2d ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → ( ( 1 ... 𝑖 ) ∖ 𝑏 ) = ( ( 1 ... 𝑖 ) ∖ 𝐶 ) )
12 11 fveq2d ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) = ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) )
13 10 12 oveq12d ⊢ ( ( 𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ ) → ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) = ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) )
14 13 mpteq2dva ⊢ ( 𝑏 = 𝐶 → ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) ) = ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) ) )
15 ineq2 ⊢ ( 𝑏 = 𝑐 → ( ( 1 ... 𝑖 ) ∩ 𝑏 ) = ( ( 1 ... 𝑖 ) ∩ 𝑐 ) )
16 15 fveq2d ⊢ ( 𝑏 = 𝑐 → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) = ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) )
17 difeq2 ⊢ ( 𝑏 = 𝑐 → ( ( 1 ... 𝑖 ) ∖ 𝑏 ) = ( ( 1 ... 𝑖 ) ∖ 𝑐 ) )
18 17 fveq2d ⊢ ( 𝑏 = 𝑐 → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) = ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) )
19 16 18 oveq12d ⊢ ( 𝑏 = 𝑐 → ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) = ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) )
20 19 mpteq2dv ⊢ ( 𝑏 = 𝑐 → ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) ) = ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
21 20 cbvmptv ⊢ ( 𝑏 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) ) ) = ( 𝑐 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑐 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑐 ) ) ) ) )
22 5 21 eqtr4i ⊢ 𝐹 = ( 𝑏 ∈ 𝑂 ↦ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝑏 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝑏 ) ) ) ) )
23 zex ⊢ ℤ ∈ V
24 23 mptex ⊢ ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) ) ∈ V
25 14 22 24 fvmpt ⊢ ( 𝐶 ∈ 𝑂 → ( 𝐹 ‘ 𝐶 ) = ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) ) )
26 6 25 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = ( 𝑖 ∈ ℤ ↦ ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) ) )
27 oveq2 ⊢ ( 𝑖 = 𝐽 → ( 1 ... 𝑖 ) = ( 1 ... 𝐽 ) )
28 27 ineq1d ⊢ ( 𝑖 = 𝐽 → ( ( 1 ... 𝑖 ) ∩ 𝐶 ) = ( ( 1 ... 𝐽 ) ∩ 𝐶 ) )
29 28 fveq2d ⊢ ( 𝑖 = 𝐽 → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) = ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) )
30 27 difeq1d ⊢ ( 𝑖 = 𝐽 → ( ( 1 ... 𝑖 ) ∖ 𝐶 ) = ( ( 1 ... 𝐽 ) ∖ 𝐶 ) )
31 30 fveq2d ⊢ ( 𝑖 = 𝐽 → ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) = ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) )
32 29 31 oveq12d ⊢ ( 𝑖 = 𝐽 → ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑖 = 𝐽 ) → ( ( ♯ ‘ ( ( 1 ... 𝑖 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝑖 ) ∖ 𝐶 ) ) ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )
34 ovexd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) ∈ V )
35 26 33 7 34 fvmptd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ‘ 𝐽 ) = ( ( ♯ ‘ ( ( 1 ... 𝐽 ) ∩ 𝐶 ) ) − ( ♯ ‘ ( ( 1 ... 𝐽 ) ∖ 𝐶 ) ) ) )