Theorem 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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	tsmspropd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	tsmspropd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
	tsmspropd.b	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
	tsmspropd.p	⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
	tsmspropd.j	⊢ ( 𝜑 → ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐻 ) )
Assertion	tsmspropd	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐻 tsums 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		tsmspropd.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		tsmspropd.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3		tsmspropd.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑋 )
4		tsmspropd.b	⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐻 ) )
5		tsmspropd.p	⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
6		tsmspropd.j	⊢ ( 𝜑 → ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐻 ) )
7	6	oveq1d	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) = ( ( TopOpen ‘ 𝐻 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) )
8	1	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑦 ) ∈ V )
9	8 2 3 4 5	gsumpropd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) = ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) )
10	9	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ) )
11	7 10	fveq12d	⊢ ( 𝜑 → ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) = ( ( ( TopOpen ‘ 𝐻 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
12		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
13		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
14		eqid	⊢ ( 𝒫 dom 𝐹 ∩ Fin ) = ( 𝒫 dom 𝐹 ∩ Fin )
15		eqid	⊢ ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) = ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } )
16		eqidd	⊢ ( 𝜑 → dom 𝐹 = dom 𝐹 )
17	12 13 14 15 2 1 16	tsmsval2	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
18		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
19		eqid	⊢ ( TopOpen ‘ 𝐻 ) = ( TopOpen ‘ 𝐻 )
20	18 19 14 15 3 1 16	tsmsval2	⊢ ( 𝜑 → ( 𝐻 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐻 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
21	11 17 20	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐻 tsums 𝐹 ) )