esummulc1

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

	Ref	Expression
Hypotheses	esummulc2.a	$⊢ φ \to A \in V$
	esummulc2.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esummulc2.c	$⊢ φ \to C \in [0, +∞)$
Assertion	esummulc1	$⊢ φ \to \underset{k \in A}{\sum^{}} B \cdot_{𝑒} C = \underset{k \in A}{\sum^{}} (B \cdot_{𝑒} C)$

Proof

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

Metamath Proof Explorer

Theorem esummulc1

Proof