Step | Hyp | Ref
| Expression |
1 | | ballotlemfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑂) |
2 | | simpl 486 |
. . . . . . . 8
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → 𝑏 = 𝐶) |
3 | 2 | ineq2d 4101 |
. . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝐶)) |
4 | 3 | fveq2d 6672 |
. . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
(♯‘((1...𝑖)
∩ 𝑏)) =
(♯‘((1...𝑖)
∩ 𝐶))) |
5 | 2 | difeq2d 4011 |
. . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝐶)) |
6 | 5 | fveq2d 6672 |
. . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
(♯‘((1...𝑖)
∖ 𝑏)) =
(♯‘((1...𝑖)
∖ 𝐶))) |
7 | 4, 6 | oveq12d 7182 |
. . . . 5
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) →
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))) =
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶)))) |
8 | 7 | mpteq2dva 5122 |
. . . 4
⊢ (𝑏 = 𝐶 → (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏)))) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) |
9 | | ballotth.f |
. . . . 5
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
10 | | ineq2 4095 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝑐)) |
11 | 10 | fveq2d 6672 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (♯‘((1...𝑖) ∩ 𝑏)) = (♯‘((1...𝑖) ∩ 𝑐))) |
12 | | difeq2 4005 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝑐)) |
13 | 12 | fveq2d 6672 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (♯‘((1...𝑖) ∖ 𝑏)) = (♯‘((1...𝑖) ∖ 𝑐))) |
14 | 11, 13 | oveq12d 7182 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → ((♯‘((1...𝑖) ∩ 𝑏)) − (♯‘((1...𝑖) ∖ 𝑏))) = ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))) |
15 | 14 | mpteq2dv 5123 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏)))) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
16 | 15 | cbvmptv 5130 |
. . . . 5
⊢ (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))))) = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑐)) −
(♯‘((1...𝑖)
∖ 𝑐))))) |
17 | 9, 16 | eqtr4i 2764 |
. . . 4
⊢ 𝐹 = (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝑏)) −
(♯‘((1...𝑖)
∖ 𝑏))))) |
18 | | zex 12064 |
. . . . 5
⊢ ℤ
∈ V |
19 | 18 | mptex 6990 |
. . . 4
⊢ (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶)))) ∈
V |
20 | 8, 17, 19 | fvmpt 6769 |
. . 3
⊢ (𝐶 ∈ 𝑂 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) |
21 | 1, 20 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦
((♯‘((1...𝑖)
∩ 𝐶)) −
(♯‘((1...𝑖)
∖ 𝐶))))) |
22 | | oveq2 7172 |
. . . . . 6
⊢ (𝑖 = 𝐽 → (1...𝑖) = (1...𝐽)) |
23 | 22 | ineq1d 4100 |
. . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∩ 𝐶) = ((1...𝐽) ∩ 𝐶)) |
24 | 23 | fveq2d 6672 |
. . . 4
⊢ (𝑖 = 𝐽 → (♯‘((1...𝑖) ∩ 𝐶)) = (♯‘((1...𝐽) ∩ 𝐶))) |
25 | 22 | difeq1d 4010 |
. . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∖ 𝐶) = ((1...𝐽) ∖ 𝐶)) |
26 | 25 | fveq2d 6672 |
. . . 4
⊢ (𝑖 = 𝐽 → (♯‘((1...𝑖) ∖ 𝐶)) = (♯‘((1...𝐽) ∖ 𝐶))) |
27 | 24, 26 | oveq12d 7182 |
. . 3
⊢ (𝑖 = 𝐽 → ((♯‘((1...𝑖) ∩ 𝐶)) − (♯‘((1...𝑖) ∖ 𝐶))) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) |
28 | 27 | adantl 485 |
. 2
⊢ ((𝜑 ∧ 𝑖 = 𝐽) → ((♯‘((1...𝑖) ∩ 𝐶)) − (♯‘((1...𝑖) ∖ 𝐶))) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) |
29 | | ballotlemfval.j |
. 2
⊢ (𝜑 → 𝐽 ∈ ℤ) |
30 | | ovexd 7199 |
. 2
⊢ (𝜑 →
((♯‘((1...𝐽)
∩ 𝐶)) −
(♯‘((1...𝐽)
∖ 𝐶))) ∈
V) |
31 | 21, 28, 29, 30 | fvmptd 6776 |
1
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) |