Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
((ordTop‘ ≤ ) ↾t (0[,]+∞)) |
2 | | esummulc2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | esummulc2.b |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
4 | | eqid 2738 |
. . . 4
⊢ (𝑧 ∈ (0[,]+∞) ↦
(𝑧 ·e
𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) |
5 | | esummulc2.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
6 | 1, 4, 5 | xrge0mulc1cn 31463 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) ∈ (((ordTop‘ ≤
) ↾t (0[,]+∞)) Cn ((ordTop‘ ≤ )
↾t (0[,]+∞)))) |
7 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))) |
8 | | oveq1 7178 |
. . . . 5
⊢ (𝑧 = 0 → (𝑧 ·e 𝐶) = (0 ·e 𝐶)) |
9 | | icossxr 12907 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ* |
10 | 9, 5 | sseldi 3876 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
11 | | xmul02 12745 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ (0 ·e 𝐶) = 0) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ·e
𝐶) = 0) |
13 | 8, 12 | sylan9eqr 2795 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = 0) → (𝑧 ·e 𝐶) = 0) |
14 | | 0e0iccpnf 12934 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈
(0[,]+∞)) |
16 | 7, 13, 15, 15 | fvmptd 6783 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘0) =
0) |
17 | | simp2 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝑥 ∈
(0[,]+∞)) |
18 | | simp3 1139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝑦 ∈
(0[,]+∞)) |
19 | | icossicc 12911 |
. . . . . 6
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
20 | 5 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝐶 ∈
(0[,)+∞)) |
21 | 19, 20 | sseldi 3876 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
𝐶 ∈
(0[,]+∞)) |
22 | | xrge0adddir 30878 |
. . . . 5
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞)
∧ 𝐶 ∈
(0[,]+∞)) → ((𝑥
+𝑒 𝑦)
·e 𝐶) =
((𝑥 ·e
𝐶) +𝑒
(𝑦 ·e
𝐶))) |
23 | 17, 18, 21, 22 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑥 +𝑒
𝑦) ·e
𝐶) = ((𝑥 ·e 𝐶) +𝑒 (𝑦 ·e 𝐶))) |
24 | | eqidd 2739 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶)) =
(𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))) |
25 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = (𝑥 +𝑒 𝑦)) → 𝑧 = (𝑥 +𝑒 𝑦)) |
26 | 25 | oveq1d 7186 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = (𝑥 +𝑒 𝑦)) → (𝑧 ·e 𝐶) = ((𝑥 +𝑒 𝑦) ·e 𝐶)) |
27 | | ge0xaddcl 12937 |
. . . . . 6
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝑦 ∈ (0[,]+∞))
→ (𝑥
+𝑒 𝑦)
∈ (0[,]+∞)) |
28 | 27 | 3adant1 1131 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑥 +𝑒
𝑦) ∈
(0[,]+∞)) |
29 | | ovexd 7206 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑥 +𝑒
𝑦) ·e
𝐶) ∈
V) |
30 | 24, 26, 28, 29 | fvmptd 6783 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘(𝑥 +𝑒 𝑦)) = ((𝑥 +𝑒 𝑦) ·e 𝐶)) |
31 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑥) → 𝑧 = 𝑥) |
32 | 31 | oveq1d 7186 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑥) → (𝑧 ·e 𝐶) = (𝑥 ·e 𝐶)) |
33 | | ovexd 7206 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑥 ·e
𝐶) ∈
V) |
34 | 24, 32, 17, 33 | fvmptd 6783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑥) = (𝑥 ·e 𝐶)) |
35 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑦) → 𝑧 = 𝑦) |
36 | 35 | oveq1d 7186 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) ∧
𝑧 = 𝑦) → (𝑧 ·e 𝐶) = (𝑦 ·e 𝐶)) |
37 | | ovexd 7206 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(𝑦 ·e
𝐶) ∈
V) |
38 | 24, 36, 18, 37 | fvmptd 6783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑦) = (𝑦 ·e 𝐶)) |
39 | 34, 38 | oveq12d 7189 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
(((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘𝑥) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑦)) = ((𝑥 ·e 𝐶) +𝑒 (𝑦 ·e 𝐶))) |
40 | 23, 30, 39 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞)) →
((𝑧 ∈ (0[,]+∞)
↦ (𝑧
·e 𝐶))‘(𝑥 +𝑒 𝑦)) = (((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑥) +𝑒 ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝑦))) |
41 | 1, 2, 3, 6, 16, 40 | esumcocn 31618 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘Σ*𝑘 ∈ 𝐴𝐵) = Σ*𝑘 ∈ 𝐴((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵)) |
42 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) → 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) |
43 | 42 | oveq1d 7186 |
. . 3
⊢ ((𝜑 ∧ 𝑧 = Σ*𝑘 ∈ 𝐴𝐵) → (𝑧 ·e 𝐶) = (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶)) |
44 | 3 | ralrimiva 3096 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) |
45 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑘𝐴 |
46 | 45 | esumcl 31568 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ (0[,]+∞)) →
Σ*𝑘 ∈
𝐴𝐵 ∈ (0[,]+∞)) |
47 | 2, 44, 46 | syl2anc 587 |
. . 3
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 ∈ (0[,]+∞)) |
48 | | ovexd 7206 |
. . 3
⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) ∈ V) |
49 | 7, 43, 47, 48 | fvmptd 6783 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘Σ*𝑘 ∈ 𝐴𝐵) = (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶)) |
50 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶)) = (𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))) |
51 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
52 | 51 | oveq1d 7186 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 = 𝐵) → (𝑧 ·e 𝐶) = (𝐵 ·e 𝐶)) |
53 | | ovexd 7206 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 ·e 𝐶) ∈ V) |
54 | 50, 52, 3, 53 | fvmptd 6783 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵) = (𝐵 ·e 𝐶)) |
55 | 54 | esumeq2dv 31576 |
. 2
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴((𝑧 ∈ (0[,]+∞) ↦ (𝑧 ·e 𝐶))‘𝐵) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) |
56 | 41, 49, 55 | 3eqtr3d 2781 |
1
⊢ (𝜑 → (Σ*𝑘 ∈ 𝐴𝐵 ·e 𝐶) = Σ*𝑘 ∈ 𝐴(𝐵 ·e 𝐶)) |