This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) )