Proof of Theorem indsumin
| Step | Hyp | Ref
| Expression |
| 1 | | inindif 4375 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) |
| 3 | | inundif 4479 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
| 4 | 3 | eqcomi 2746 |
. . . 4
⊢ 𝐴 = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐴 = ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) |
| 6 | | indsumin.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 7 | | pr01ssre 32826 |
. . . . . 6
⊢ {0, 1}
⊆ ℝ |
| 8 | | ax-resscn 11212 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
| 9 | 7, 8 | sstri 3993 |
. . . . 5
⊢ {0, 1}
⊆ ℂ |
| 10 | | indsumin.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 11 | | indsumin.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ 𝑂) |
| 12 | | indf 32840 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐵):𝑂⟶{0, 1}) |
| 13 | 10, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝟭‘𝑂)‘𝐵):𝑂⟶{0, 1}) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝟭‘𝑂)‘𝐵):𝑂⟶{0, 1}) |
| 15 | | indsumin.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑂) |
| 16 | 15 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑂) |
| 17 | 14, 16 | ffvelcdmd 7105 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐵)‘𝑘) ∈ {0, 1}) |
| 18 | 9, 17 | sselid 3981 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐵)‘𝑘) ∈ ℂ) |
| 19 | | indsumin.5 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 20 | 18, 19 | mulcld 11281 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) ∈ ℂ) |
| 21 | 2, 5, 6, 20 | fsumsplit 15777 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = (Σ𝑘 ∈ (𝐴 ∩ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) + Σ𝑘 ∈ (𝐴 ∖ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶))) |
| 22 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → 𝑂 ∈ 𝑉) |
| 23 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → 𝐵 ⊆ 𝑂) |
| 24 | | inss2 4238 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
| 25 | 24 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐵) |
| 26 | 25 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → 𝑘 ∈ 𝐵) |
| 27 | | ind1 32842 |
. . . . . . 7
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ 𝐵) → (((𝟭‘𝑂)‘𝐵)‘𝑘) = 1) |
| 28 | 22, 23, 26, 27 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → (((𝟭‘𝑂)‘𝐵)‘𝑘) = 1) |
| 29 | 28 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = (1 · 𝐶)) |
| 30 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐴) |
| 32 | 31 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → 𝑘 ∈ 𝐴) |
| 33 | 32, 19 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → 𝐶 ∈ ℂ) |
| 34 | 33 | mullidd 11279 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → (1 · 𝐶) = 𝐶) |
| 35 | 29, 34 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∩ 𝐵)) → ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = 𝐶) |
| 36 | 35 | sumeq2dv 15738 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∩ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶) |
| 37 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → 𝑂 ∈ 𝑉) |
| 38 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → 𝐵 ⊆ 𝑂) |
| 39 | 15 | ssdifd 4145 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ (𝑂 ∖ 𝐵)) |
| 40 | 39 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → 𝑘 ∈ (𝑂 ∖ 𝐵)) |
| 41 | | ind0 32843 |
. . . . . . . 8
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ (𝑂 ∖ 𝐵)) → (((𝟭‘𝑂)‘𝐵)‘𝑘) = 0) |
| 42 | 37, 38, 40, 41 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → (((𝟭‘𝑂)‘𝐵)‘𝑘) = 0) |
| 43 | 42 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = (0 · 𝐶)) |
| 44 | | difssd 4137 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴) |
| 45 | 44 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → 𝑘 ∈ 𝐴) |
| 46 | 45, 19 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → 𝐶 ∈ ℂ) |
| 47 | 46 | mul02d 11459 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → (0 · 𝐶) = 0) |
| 48 | 43, 47 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐵)) → ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = 0) |
| 49 | 48 | sumeq2dv 15738 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∖ 𝐵)0) |
| 50 | | diffi 9215 |
. . . . . 6
⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin) |
| 51 | 6, 50 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∖ 𝐵) ∈ Fin) |
| 52 | | sumz 15758 |
. . . . . 6
⊢ (((𝐴 ∖ 𝐵) ⊆ (ℤ≥‘0)
∨ (𝐴 ∖ 𝐵) ∈ Fin) →
Σ𝑘 ∈ (𝐴 ∖ 𝐵)0 = 0) |
| 53 | 52 | olcs 877 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∈ Fin → Σ𝑘 ∈ (𝐴 ∖ 𝐵)0 = 0) |
| 54 | 51, 53 | syl 17 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ 𝐵)0 = 0) |
| 55 | 49, 54 | eqtrd 2777 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∖ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = 0) |
| 56 | 36, 55 | oveq12d 7449 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ (𝐴 ∩ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) + Σ𝑘 ∈ (𝐴 ∖ 𝐵)((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶)) = (Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶 + 0)) |
| 57 | | infi 9302 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝐴 ∩ 𝐵) ∈ Fin) |
| 58 | 6, 57 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ Fin) |
| 59 | 58, 33 | fsumcl 15769 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶 ∈ ℂ) |
| 60 | 59 | addridd 11461 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶 + 0) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶) |
| 61 | 21, 56, 60 | 3eqtrd 2781 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶) |