tsmspropd

Description: The group sum depends only on the base set, additive operation, and topology components. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd etc. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tsmspropd.f	$⊢ φ \to F \in V$
	tsmspropd.g	$⊢ φ \to G \in W$
	tsmspropd.h	$⊢ φ \to H \in X$
	tsmspropd.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
	tsmspropd.p	$⊢ φ \to +_{G} = +_{H}$
	tsmspropd.j	$⊢ φ \to TopOpen (G) = TopOpen (H)$
Assertion	tsmspropd	$⊢ φ \to G tsums F = H tsums F$

Proof

Step	Hyp	Ref	Expression
1		tsmspropd.f	$⊢ φ \to F \in V$
2		tsmspropd.g	$⊢ φ \to G \in W$
3		tsmspropd.h	$⊢ φ \to H \in X$
4		tsmspropd.b	$⊢ φ \to {Base}_{G} = {Base}_{H}$
5		tsmspropd.p	$⊢ φ \to +_{G} = +_{H}$
6		tsmspropd.j	$⊢ φ \to TopOpen (G) = TopOpen (H)$
7	6	oveq1d	$⊢ φ \to TopOpen (G) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\})) = TopOpen (H) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}))$
8		resexg	$⊢ F \in V \to {F ↾}_{y} \in V$
9	1 8	syl	$⊢ φ \to {F ↾}_{y} \in V$
10	9 2 3 4 5	gsumpropd	$⊢ φ \to \sum_{G} ({F ↾}_{y}) = \sum_{H} ({F ↾}_{y})$
11	10	mpteq2dv	$⊢ φ \to (y \in (𝒫 dom F \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})) = (y \in (𝒫 dom F \cap Fin) ⟼ \sum_{H} ({F ↾}_{y}))$
12	7 11	fveq12d	$⊢ φ \to (TopOpen (G) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}))) ((y \in (𝒫 dom F \cap Fin) ⟼ \sum_{G} ({F ↾}_{y}))) = (TopOpen (H) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}))) ((y \in (𝒫 dom F \cap Fin) ⟼ \sum_{H} ({F ↾}_{y})))$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14		eqid	$⊢ TopOpen (G) = TopOpen (G)$
15		eqid	$⊢ 𝒫 dom F \cap Fin = 𝒫 dom F \cap Fin$
16		eqid	$⊢ ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}) = ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\})$
17		eqidd	$⊢ φ \to dom F = dom F$
18	13 14 15 16 2 1 17	tsmsval2	$⊢ φ \to G tsums F = (TopOpen (G) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}))) ((y \in (𝒫 dom F \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})))$
19		eqid	$⊢ {Base}_{H} = {Base}_{H}$
20		eqid	$⊢ TopOpen (H) = TopOpen (H)$
21	19 20 15 16 3 1 17	tsmsval2	$⊢ φ \to H tsums F = (TopOpen (H) fLimf ((𝒫 dom F \cap Fin) filGen ran (z \in (𝒫 dom F \cap Fin) ⟼ \{y \in (𝒫 dom F \cap Fin) \| z \subseteq y\}))) ((y \in (𝒫 dom F \cap Fin) ⟼ \sum_{H} ({F ↾}_{y})))$
22	12 18 21	3eqtr4d	$⊢ φ \to G tsums F = H tsums F$

Metamath Proof Explorer

Theorem tsmspropd

Proof