Metamath Proof Explorer

Theorem esummulc1

Description: An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses esummulc2.a ⊢ φ → A ∈ V
esummulc2.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esummulc2.c ⊢ φ → C ∈ 0 +∞
Assertion esummulc1 ⊢ φ → ∑ * k ∈ A B ⋅ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 C

Proof

Step Hyp Ref Expression
1 esummulc2.a ⊢ φ → A ∈ V
2 esummulc2.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
3 esummulc2.c ⊢ φ → C ∈ 0 +∞
4 eqid ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
5 eqid ⊢ z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C = z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C
6 4 5 3 xrge0mulc1cn ⊢ φ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ∈ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
7 eqidd ⊢ φ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C = z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C
8 oveq1 ⊢ z = 0 → z ⋅ 𝑒 C = 0 ⋅ 𝑒 C
9 icossxr ⊢ 0 +∞ ⊆ ℝ *
10 9 3 sselid ⊢ φ → C ∈ ℝ *
11 xmul02 ⊢ C ∈ ℝ * → 0 ⋅ 𝑒 C = 0
12 10 11 syl ⊢ φ → 0 ⋅ 𝑒 C = 0
13 8 12 sylan9eqr ⊢ φ ∧ z = 0 → z ⋅ 𝑒 C = 0
14 0e0iccpnf ⊢ 0 ∈ 0 +∞
15 14 a1i ⊢ φ → 0 ∈ 0 +∞
16 7 13 15 15 fvmptd ⊢ φ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ 0 = 0
17 simp2 ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ∈ 0 +∞
18 simp3 ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ∈ 0 +∞
19 icossicc ⊢ 0 +∞ ⊆ 0 +∞
20 3 3ad2ant1 ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → C ∈ 0 +∞
21 19 20 sselid ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → C ∈ 0 +∞
22 xrge0adddir ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ C ∈ 0 +∞ → x + 𝑒 y ⋅ 𝑒 C = x ⋅ 𝑒 C + 𝑒 y ⋅ 𝑒 C
23 17 18 21 22 syl3anc ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + 𝑒 y ⋅ 𝑒 C = x ⋅ 𝑒 C + 𝑒 y ⋅ 𝑒 C
24 eqidd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C = z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C
25 simpr ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = x + 𝑒 y → z = x + 𝑒 y
26 25 oveq1d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = x + 𝑒 y → z ⋅ 𝑒 C = x + 𝑒 y ⋅ 𝑒 C
27 ge0xaddcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + 𝑒 y ∈ 0 +∞
28 27 3adant1 ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + 𝑒 y ∈ 0 +∞
29 ovexd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + 𝑒 y ⋅ 𝑒 C ∈ V
30 24 26 28 29 fvmptd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ x + 𝑒 y = x + 𝑒 y ⋅ 𝑒 C
31 simpr ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = x → z = x
32 31 oveq1d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = x → z ⋅ 𝑒 C = x ⋅ 𝑒 C
33 ovexd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ⋅ 𝑒 C ∈ V
34 24 32 17 33 fvmptd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ x = x ⋅ 𝑒 C
35 simpr ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = y → z = y
36 35 oveq1d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ ∧ z = y → z ⋅ 𝑒 C = y ⋅ 𝑒 C
37 ovexd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → y ⋅ 𝑒 C ∈ V
38 24 36 18 37 fvmptd ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ y = y ⋅ 𝑒 C
39 34 38 oveq12d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ x + 𝑒 z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ y = x ⋅ 𝑒 C + 𝑒 y ⋅ 𝑒 C
40 23 30 39 3eqtr4d ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ x + 𝑒 y = z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ x + 𝑒 z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ y
41 4 1 2 6 16 40 esumcocn ⊢ φ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ ∑ * k ∈ A B = ∑ * k ∈ A z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ B
42 simpr ⊢ φ ∧ z = ∑ * k ∈ A B → z = ∑ * k ∈ A B
43 42 oveq1d ⊢ φ ∧ z = ∑ * k ∈ A B → z ⋅ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 C
44 2 ralrimiva ⊢ φ → ∀ k ∈ A B ∈ 0 +∞
45 nfcv ⊢ Ⅎ _ k A
46 45 esumcl ⊢ A ∈ V ∧ ∀ k ∈ A B ∈ 0 +∞ → ∑ * k ∈ A B ∈ 0 +∞
47 1 44 46 syl2anc ⊢ φ → ∑ * k ∈ A B ∈ 0 +∞
48 ovexd ⊢ φ → ∑ * k ∈ A B ⋅ 𝑒 C ∈ V
49 7 43 47 48 fvmptd ⊢ φ → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ ∑ * k ∈ A B = ∑ * k ∈ A B ⋅ 𝑒 C
50 eqidd ⊢ φ ∧ k ∈ A → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C = z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C
51 simpr ⊢ φ ∧ k ∈ A ∧ z = B → z = B
52 51 oveq1d ⊢ φ ∧ k ∈ A ∧ z = B → z ⋅ 𝑒 C = B ⋅ 𝑒 C
53 ovexd ⊢ φ ∧ k ∈ A → B ⋅ 𝑒 C ∈ V
54 50 52 2 53 fvmptd ⊢ φ ∧ k ∈ A → z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ B = B ⋅ 𝑒 C
55 54 esumeq2dv ⊢ φ → ∑ * k ∈ A z ∈ 0 +∞ ⟼ z ⋅ 𝑒 C ⁡ B = ∑ * k ∈ A B ⋅ 𝑒 C
56 41 49 55 3eqtr3d ⊢ φ → ∑ * k ∈ A B ⋅ 𝑒 C = ∑ * k ∈ A B ⋅ 𝑒 C