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	1	resexd	$⊢ φ \to {F ↾}_{y} \in V$
9	8 2 3 4 5	gsumpropd	$⊢ φ \to \sum_{G} ({F ↾}_{y}) = \sum_{H} ({F ↾}_{y})$
10	9	mpteq2dv	$⊢ φ \to (y \in (𝒫 dom F \cap Fin) ⟼ \sum_{G} ({F ↾}_{y})) = (y \in (𝒫 dom F \cap Fin) ⟼ \sum_{H} ({F ↾}_{y}))$
11	7 10	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})))$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13		eqid	$⊢ TopOpen (G) = TopOpen (G)$
14		eqid	$⊢ 𝒫 dom F \cap Fin = 𝒫 dom F \cap Fin$
15		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\})$
16		eqidd	$⊢ φ \to dom F = dom F$
17	12 13 14 15 2 1 16	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})))$
18		eqid	$⊢ {Base}_{H} = {Base}_{H}$
19		eqid	$⊢ TopOpen (H) = TopOpen (H)$
20	18 19 14 15 3 1 16	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})))$
21	11 17 20	3eqtr4d	$⊢ φ \to G tsums F = H tsums F$

Metamath Proof Explorer

Theorem tsmspropd

Proof