| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
((ordTop‘ ≤ ) ↾t (0[,]+∞)) |
| 2 | | esummulc2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | | esummulc2.b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
| 4 | | eqid 2737 |
. . . 4
⊢ (𝑧 ∈ (0[,]+∞) ↦
(𝑧 ·e
𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) |
| 5 | | esummulc2.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
| 6 | 1, 4, 5 | xrge0mulc1cn 33940 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) ∈ (((ordTop‘ ≤
) ↾t (0[,]+∞)) Cn ((ordTop‘ ≤ )
↾t (0[,]+∞)))) |
| 7 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))) |
| 8 | | oveq1 7438 |
. . . . 5
⊢ (𝑧 = 0 → (𝑧 ·e 𝐶) = (0 ·e 𝐶)) |
| 9 | | icossxr 13472 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ* |
| 10 | 9, 5 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 11 | | xmul02 13310 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ (0 ·e 𝐶) = 0) |
| 12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ·e
𝐶) = 0) |
| 13 | 8, 12 | sylan9eqr 2799 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 0) → (𝑧 ·e 𝐶) = 0) |
| 14 | | 0e0iccpnf 13499 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
| 15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]+∞)) |
| 16 | 7, 13, 15, 15 | fvmptd 7023 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘0) =
0) |
| 17 | | simp2 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
| 18 | | simp3 1139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝑦 ∈
(0[,]+∞)) |
| 19 | | icossicc 13476 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
| 20 | 5 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝐶 ∈
(0[,)+∞)) |
| 21 | 19, 20 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝐶 ∈
(0[,]+∞)) |
| 22 | | xrge0adddir 33023 |
. . . . 5
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → ((𝑥
+𝑒 𝑦)
·e 𝐶) =
((𝑥 ·e
𝐶) +𝑒
(𝑦 ·e
𝐶))) |
| 23 | 17, 18, 21, 22 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑥 +𝑒
𝑦) ·e
𝐶) = ((𝑥 ·e 𝐶) +𝑒 (𝑦 ·e 𝐶))) |
| 24 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶)) =
(𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))) |
| 25 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = (𝑥 +𝑒 𝑦)) → 𝑧 = (𝑥 +𝑒 𝑦)) |
| 26 | 25 | oveq1d 7446 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = (𝑥 +𝑒 𝑦)) → (𝑧 ·e 𝐶) = ((𝑥 +𝑒 𝑦) ·e 𝐶)) |
| 27 | | ge0xaddcl 13502 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞))
→ (𝑥
+𝑒 𝑦)
∈ (0[,]+∞)) |
| 28 | 27 | 3adant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑥 +𝑒
𝑦) ∈
(0[,]+∞)) |
| 29 | | ovexd 7466 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑥 +𝑒
𝑦) ·e
𝐶) ∈
V) |
| 30 | 24, 26, 28, 29 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘(𝑥 +𝑒 𝑦)) = ((𝑥 +𝑒 𝑦) ·e 𝐶)) |
| 31 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑥) → 𝑧 = 𝑥) |
| 32 | 31 | oveq1d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑥) → (𝑧 ·e 𝐶) = (𝑥 ·e 𝐶)) |
| 33 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑥 ·e
𝐶) ∈
V) |
| 34 | 24, 32, 17, 33 | fvmptd 7023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑥) = (𝑥 ·e 𝐶)) |
| 35 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑦) → 𝑧 = 𝑦) |
| 36 | 35 | oveq1d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑦) → (𝑧 ·e 𝐶) = (𝑦 ·e 𝐶)) |
| 37 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑦 ·e
𝐶) ∈
V) |
| 38 | 24, 36, 18, 37 | fvmptd 7023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑦) = (𝑦 ·e 𝐶)) |
| 39 | 34, 38 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑥) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑦)) = ((𝑥 ·e 𝐶) +𝑒 (𝑦 ·e 𝐶))) |
| 40 | 23, 30, 39 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘(𝑥 +𝑒 𝑦)) = (((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑥) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑦))) |
| 41 | 1, 2, 3, 6, 16, 40 | esumcocn 34081 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵)) |
| 42 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) → 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) |
| 43 | 42 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) → (𝑧 ·e 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶)) |
| 44 | 3 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) |
| 45 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘𝐴 |
| 46 | 45 | esumcl 34031 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 ∈ (0[,]+∞)) |
| 47 | 2, 44, 46 | syl2anc 584 |
. . 3
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞)) |
| 48 | | ovexd 7466 |
. . 3
⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) ∈ V) |
| 49 | 7, 43, 47, 48 | fvmptd 7023 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘Σ*𝑘 ∈ 𝐴𝐵) = (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶)) |
| 50 | | eqidd 2738 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))) |
| 51 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
| 52 | 51 | oveq1d 7446 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 = 𝐵) → (𝑧 ·e 𝐶) = (𝐵 ·e 𝐶)) |
| 53 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 ·e 𝐶) ∈ V) |
| 54 | 50, 52, 3, 53 | fvmptd 7023 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵) = (𝐵 ·e 𝐶)) |
| 55 | 54 | esumeq2dv 34039 |
. 2
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) |
| 56 | 41, 49, 55 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) |