Step | Hyp | Ref
| Expression |
1 | | ballotlemfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑂) |
2 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → 𝑏 = 𝐶) |
3 | 2 | ineq2d 3814 |
. . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝐶)) |
4 | 3 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → (#‘((1...𝑖) ∩ 𝑏)) = (#‘((1...𝑖) ∩ 𝐶))) |
5 | 2 | difeq2d 3728 |
. . . . . . 7
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝐶)) |
6 | 5 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → (#‘((1...𝑖) ∖ 𝑏)) = (#‘((1...𝑖) ∖ 𝐶))) |
7 | 4, 6 | oveq12d 6668 |
. . . . 5
⊢ ((𝑏 = 𝐶 ∧ 𝑖 ∈ ℤ) → ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏))) = ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶)))) |
8 | 7 | mpteq2dva 4744 |
. . . 4
⊢ (𝑏 = 𝐶 → (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏)))) = (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶))))) |
9 | | ballotth.f |
. . . . 5
⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) |
10 | | ineq2 3808 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∩ 𝑏) = ((1...𝑖) ∩ 𝑐)) |
11 | 10 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (#‘((1...𝑖) ∩ 𝑏)) = (#‘((1...𝑖) ∩ 𝑐))) |
12 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑏 = 𝑐 → ((1...𝑖) ∖ 𝑏) = ((1...𝑖) ∖ 𝑐)) |
13 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑏 = 𝑐 → (#‘((1...𝑖) ∖ 𝑏)) = (#‘((1...𝑖) ∖ 𝑐))) |
14 | 11, 13 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑏 = 𝑐 → ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏))) = ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐)))) |
15 | 14 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏)))) = (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) |
16 | 15 | cbvmptv 4750 |
. . . . 5
⊢ (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏))))) = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑐)) − (#‘((1...𝑖) ∖ 𝑐))))) |
17 | 9, 16 | eqtr4i 2647 |
. . . 4
⊢ 𝐹 = (𝑏 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝑏)) − (#‘((1...𝑖) ∖ 𝑏))))) |
18 | | zex 11386 |
. . . . 5
⊢ ℤ
∈ V |
19 | 18 | mptex 6486 |
. . . 4
⊢ (𝑖 ∈ ℤ ↦
((#‘((1...𝑖) ∩
𝐶)) −
(#‘((1...𝑖) ∖
𝐶)))) ∈
V |
20 | 8, 17, 19 | fvmpt 6282 |
. . 3
⊢ (𝐶 ∈ 𝑂 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶))))) |
21 | 1, 20 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘𝐶) = (𝑖 ∈ ℤ ↦ ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶))))) |
22 | | oveq2 6658 |
. . . . . 6
⊢ (𝑖 = 𝐽 → (1...𝑖) = (1...𝐽)) |
23 | 22 | ineq1d 3813 |
. . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∩ 𝐶) = ((1...𝐽) ∩ 𝐶)) |
24 | 23 | fveq2d 6195 |
. . . 4
⊢ (𝑖 = 𝐽 → (#‘((1...𝑖) ∩ 𝐶)) = (#‘((1...𝐽) ∩ 𝐶))) |
25 | 22 | difeq1d 3727 |
. . . . 5
⊢ (𝑖 = 𝐽 → ((1...𝑖) ∖ 𝐶) = ((1...𝐽) ∖ 𝐶)) |
26 | 25 | fveq2d 6195 |
. . . 4
⊢ (𝑖 = 𝐽 → (#‘((1...𝑖) ∖ 𝐶)) = (#‘((1...𝐽) ∖ 𝐶))) |
27 | 24, 26 | oveq12d 6668 |
. . 3
⊢ (𝑖 = 𝐽 → ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶))) = ((#‘((1...𝐽) ∩ 𝐶)) − (#‘((1...𝐽) ∖ 𝐶)))) |
28 | 27 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑖 = 𝐽) → ((#‘((1...𝑖) ∩ 𝐶)) − (#‘((1...𝑖) ∖ 𝐶))) = ((#‘((1...𝐽) ∩ 𝐶)) − (#‘((1...𝐽) ∖ 𝐶)))) |
29 | | ballotlemfval.j |
. 2
⊢ (𝜑 → 𝐽 ∈ ℤ) |
30 | | ovexd 6680 |
. 2
⊢ (𝜑 → ((#‘((1...𝐽) ∩ 𝐶)) − (#‘((1...𝐽) ∖ 𝐶))) ∈ V) |
31 | 21, 28, 29, 30 | fvmptd 6288 |
1
⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((#‘((1...𝐽) ∩ 𝐶)) − (#‘((1...𝐽) ∖ 𝐶)))) |