tsmsval2

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmsval.b	$⊢ B = {Base}_{G}$
	tsmsval.j	$⊢ J = TopOpen (G)$
	tsmsval.s	$⊢ S = 𝒫 A \cap Fin$
	tsmsval.l	$⊢ L = ran (z \in S ⟼ \{y \in S \| z \subseteq y\})$
	tsmsval.g	$⊢ φ \to G \in V$
	tsmsval2.f	$⊢ φ \to F \in W$
	tsmsval2.a	$⊢ φ \to dom F = A$
Assertion	tsmsval2	$⊢ φ \to G tsums F = (J fLimf (S filGen L)) ((y \in S ⟼ \sum_{G} ({F ↾}_{y})))$

Proof

Step	Hyp	Ref	Expression
1		tsmsval.b	$⊢ B = {Base}_{G}$
2		tsmsval.j	$⊢ J = TopOpen (G)$
3		tsmsval.s	$⊢ S = 𝒫 A \cap Fin$
4		tsmsval.l	$⊢ L = ran (z \in S ⟼ \{y \in S \| z \subseteq y\})$
5		tsmsval.g	$⊢ φ \to G \in V$
6		tsmsval2.f	$⊢ φ \to F \in W$
7		tsmsval2.a	$⊢ φ \to dom F = A$
8		df-tsms	$⊢ tsums = (w \in V, f \in V ⟼ ⦋ (𝒫 dom f \cap Fin) / s ⦌ (TopOpen (w) fLimf (s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\}))) ((y \in s ⟼ \sum_{w} ({f ↾}_{y}))))$
9	8	a1i	$⊢ φ \to tsums = (w \in V, f \in V ⟼ ⦋ (𝒫 dom f \cap Fin) / s ⦌ (TopOpen (w) fLimf (s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\}))) ((y \in s ⟼ \sum_{w} ({f ↾}_{y}))))$
10		vex	$⊢ f \in V$
11	10	dmex	$⊢ dom f \in V$
12	11	pwex	$⊢ 𝒫 dom f \in V$
13	12	inex1	$⊢ 𝒫 dom f \cap Fin \in V$
14	13	a1i	$⊢ (φ \land (w = G \land f = F)) \to 𝒫 dom f \cap Fin \in V$
15		simplrl	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to w = G$
16	15	fveq2d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to TopOpen (w) = TopOpen (G)$
17	16 2	eqtr4di	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to TopOpen (w) = J$
18		id	$⊢ s = 𝒫 dom f \cap Fin \to s = 𝒫 dom f \cap Fin$
19		simprr	$⊢ (φ \land (w = G \land f = F)) \to f = F$
20	19	dmeqd	$⊢ (φ \land (w = G \land f = F)) \to dom f = dom F$
21	7	adantr	$⊢ (φ \land (w = G \land f = F)) \to dom F = A$
22	20 21	eqtrd	$⊢ (φ \land (w = G \land f = F)) \to dom f = A$
23	22	pweqd	$⊢ (φ \land (w = G \land f = F)) \to 𝒫 dom f = 𝒫 A$
24	23	ineq1d	$⊢ (φ \land (w = G \land f = F)) \to 𝒫 dom f \cap Fin = 𝒫 A \cap Fin$
25	24 3	eqtr4di	$⊢ (φ \land (w = G \land f = F)) \to 𝒫 dom f \cap Fin = S$
26	18 25	sylan9eqr	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to s = S$
27	26	rabeqdv	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to \{y \in s \| z \subseteq y\} = \{y \in S \| z \subseteq y\}$
28	26 27	mpteq12dv	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to (z \in s ⟼ \{y \in s \| z \subseteq y\}) = (z \in S ⟼ \{y \in S \| z \subseteq y\})$
29	28	rneqd	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to ran (z \in s ⟼ \{y \in s \| z \subseteq y\}) = ran (z \in S ⟼ \{y \in S \| z \subseteq y\})$
30	29 4	eqtr4di	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to ran (z \in s ⟼ \{y \in s \| z \subseteq y\}) = L$
31	26 30	oveq12d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\}) = S filGen L$
32	17 31	oveq12d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to TopOpen (w) fLimf (s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\})) = J fLimf (S filGen L)$
33		simplrr	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to f = F$
34	33	reseq1d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to {f ↾}_{y} = {F ↾}_{y}$
35	15 34	oveq12d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to \sum_{w} ({f ↾}_{y}) = \sum_{G} ({F ↾}_{y})$
36	26 35	mpteq12dv	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to (y \in s ⟼ \sum_{w} ({f ↾}_{y})) = (y \in S ⟼ \sum_{G} ({F ↾}_{y}))$
37	32 36	fveq12d	$⊢ ((φ \land (w = G \land f = F)) \land s = 𝒫 dom f \cap Fin) \to (TopOpen (w) fLimf (s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\}))) ((y \in s ⟼ \sum_{w} ({f ↾}_{y}))) = (J fLimf (S filGen L)) ((y \in S ⟼ \sum_{G} ({F ↾}_{y})))$
38	14 37	csbied	$⊢ (φ \land (w = G \land f = F)) \to ⦋ (𝒫 dom f \cap Fin) / s ⦌ (TopOpen (w) fLimf (s filGen ran (z \in s ⟼ \{y \in s \| z \subseteq y\}))) ((y \in s ⟼ \sum_{w} ({f ↾}_{y}))) = (J fLimf (S filGen L)) ((y \in S ⟼ \sum_{G} ({F ↾}_{y})))$
39	5	elexd	$⊢ φ \to G \in V$
40	6	elexd	$⊢ φ \to F \in V$
41		fvexd	$⊢ φ \to (J fLimf (S filGen L)) ((y \in S ⟼ \sum_{G} ({F ↾}_{y}))) \in V$
42	9 38 39 40 41	ovmpod	$⊢ φ \to G tsums F = (J fLimf (S filGen L)) ((y \in S ⟼ \sum_{G} ({F ↾}_{y})))$

Metamath Proof Explorer

Theorem tsmsval2

Proof