esumpfinvalf

Description: Same as esumpfinval , minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017) (Proof shortened by AV, 25-Jul-2019)

	Ref	Expression
Hypotheses	esumpfinvalf.1	$⊢ \underline{Ⅎ} k A$
	esumpfinvalf.2	$⊢ Ⅎ k φ$
	esumpfinvalf.a	$⊢ φ \to A \in Fin$
	esumpfinvalf.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
Assertion	esumpfinvalf	$⊢ φ \to \underset{k \in A}{\sum^{*}} B = \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		esumpfinvalf.1	$⊢ \underline{Ⅎ} k A$
2		esumpfinvalf.2	$⊢ Ⅎ k φ$
3		esumpfinvalf.a	$⊢ φ \to A \in Fin$
4		esumpfinvalf.b	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
5		df-esum	$⊢ \underset{k \in A}{\sum^{}} B = ⋃ ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B))$
6		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
7		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
8		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
9	8	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
10		xrge0tps	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
11	10	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
12		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
13		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
14	13 4	sselid	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
15		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
16	2 1 12 14 15	fmptdf2	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
17		c0ex	$⊢ 0 \in V$
18	17	a1i	$⊢ φ \to 0 \in V$
19	16 3 18	fdmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ B))$
20		xrge0topn	$⊢ TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]) = ordTop (\leq) ↾_{𝑡} [0, +∞]$
21	20	eqcomi	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
22		xrhaus	$⊢ ordTop (\leq) \in Haus$
23		ovex	$⊢ [0, +∞] \in V$
24		resthaus	$⊢ (ordTop (\leq) \in Haus \land [0, +∞] \in V) \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in Haus$
25	22 23 24	mp2an	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] \in Haus$
26	25	a1i	$⊢ φ \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in Haus$
27	6 7 9 11 3 16 19 21 26	haustsmsid	$⊢ φ \to (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B) = \{\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B\}$
28	27	unieqd	$⊢ φ \to ⋃ ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B)) = ⋃ \{\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B\}$
29	5 28	eqtrid	$⊢ φ \to \underset{k \in A}{\sum^{}} B = ⋃ \{\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B\}$
30		ovex	$⊢ \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B \in V$
31	30	unisn	$⊢ ⋃ \{\underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B\} = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
32	29 31	eqtrdi	$⊢ φ \to \underset{k \in A}{\sum^{}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
33		nfcv	$⊢ \underline{Ⅎ} k [0, +∞)$
34	2 1 33 4 15	fmptdf2	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞)$
35		esumpfinvallem	$⊢ (A \in Fin \land (k \in A ⟼ B) : A ⟶ [0, +∞)) \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
36	3 34 35	syl2anc	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \underset{k \in A}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B$
37		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39	37 38	sstri	$⊢ [0, +∞) \subseteq ℂ$
40	39 4	sselid	$⊢ (φ \land k \in A) \to B \in ℂ$
41	40	sbt	$⊢ [l/ k] ((φ \land k \in A) \to B \in ℂ)$
42		sbim	$⊢ [l/ k] ((φ \land k \in A) \to B \in ℂ) \leftrightarrow ([l/ k] (φ \land k \in A) \to [l/ k] B \in ℂ)$
43		sban	$⊢ [l/ k] (φ \land k \in A) \leftrightarrow ([l/ k] φ \land [l/ k] k \in A)$
44	2	sbf	$⊢ [l/ k] φ \leftrightarrow φ$
45	1	clelsb1fw	$⊢ [l/ k] k \in A \leftrightarrow l \in A$
46	44 45	anbi12i	$⊢ ([l/ k] φ \land [l/ k] k \in A) \leftrightarrow (φ \land l \in A)$
47	43 46	bitri	$⊢ [l/ k] (φ \land k \in A) \leftrightarrow (φ \land l \in A)$
48		sbsbc	$⊢ [l/ k] B \in ℂ \leftrightarrow \underset{˙}{[} l / k \underset{˙}{]} B \in ℂ$
49		sbcel1g	$⊢ l \in V \to (\underset{˙}{[} l / k \underset{˙}{]} B \in ℂ \leftrightarrow ⦋ l / k ⦌ B \in ℂ)$
50	49	elv	$⊢ \underset{˙}{[} l / k \underset{˙}{]} B \in ℂ \leftrightarrow ⦋ l / k ⦌ B \in ℂ$
51	48 50	bitri	$⊢ [l/ k] B \in ℂ \leftrightarrow ⦋ l / k ⦌ B \in ℂ$
52	47 51	imbi12i	$⊢ ([l/ k] (φ \land k \in A) \to [l/ k] B \in ℂ) \leftrightarrow ((φ \land l \in A) \to ⦋ l / k ⦌ B \in ℂ)$
53	42 52	bitri	$⊢ [l/ k] ((φ \land k \in A) \to B \in ℂ) \leftrightarrow ((φ \land l \in A) \to ⦋ l / k ⦌ B \in ℂ)$
54	41 53	mpbi	$⊢ (φ \land l \in A) \to ⦋ l / k ⦌ B \in ℂ$
55	3 54	gsumfsum	$⊢ φ \to \underset{l \in A}{\sum_{ℂ_{fld}}} ⦋ l / k ⦌ B = \sum_{l \in A} ⦋ l / k ⦌ B$
56		nfcv	$⊢ \underline{Ⅎ} l A$
57		nfcv	$⊢ \underline{Ⅎ} l B$
58		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ l / k ⦌ B$
59		csbeq1a	$⊢ k = l \to B = ⦋ l / k ⦌ B$
60	1 56 57 58 59	cbvmptf	$⊢ (k \in A ⟼ B) = (l \in A ⟼ ⦋ l / k ⦌ B)$
61	60	oveq2i	$⊢ \underset{k \in A}{\sum_{ℂ_{fld}}} B = \underset{l \in A}{\sum_{ℂ_{fld}}} ⦋ l / k ⦌ B$
62	59 57 58	cbvsum	$⊢ \sum_{k \in A} B = \sum_{l \in A} ⦋ l / k ⦌ B$
63	55 61 62	3eqtr4g	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$
64	32 36 63	3eqtr2d	$⊢ φ \to \underset{k \in A}{\sum^{*}} B = \sum_{k \in A} B$

Metamath Proof Explorer

Theorem esumpfinvalf

Proof