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		resexg	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ↾ 𝑦 ) ∈ V )
9	1 8	syl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑦 ) ∈ V )
10	9 2 3 4 5	gsumpropd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) = ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) )
11	10	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ) )
12	7 11	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 ( 𝐹 ↾ 𝑦 ) ) ) ) )
13		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
15		eqid	⊢ ( 𝒫 dom 𝐹 ∩ Fin ) = ( 𝒫 dom 𝐹 ∩ Fin )
16		eqid	⊢ ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) = ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } )
17		eqidd	⊢ ( 𝜑 → dom 𝐹 = dom 𝐹 )
18	13 14 15 16 2 1 17	tsmsval2	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
19		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
20		eqid	⊢ ( TopOpen ‘ 𝐻 ) = ( TopOpen ‘ 𝐻 )
21	19 20 15 16 3 1 17	tsmsval2	⊢ ( 𝜑 → ( 𝐻 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐻 ) fLimf ( ( 𝒫 dom 𝐹 ∩ Fin ) filGen ran ( 𝑧 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 dom 𝐹 ∩ Fin ) ↦ ( 𝐻 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
22	12 18 21	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐻 tsums 𝐹 ) )