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

Metamath Proof Explorer

Theorem tsmsval

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Hypotheses	tsmsval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
		tsmsval.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
		tsmsval.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
		tsmsval.l	⊢ 𝐿 = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
		tsmsval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
		tsmsval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
		tsmsval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	Assertion	tsmsval	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tsmsval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tsmsval.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3		tsmsval.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
4		tsmsval.l	⊢ 𝐿 = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
5		tsmsval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
6		tsmsval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
7		tsmsval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8	1	fvexi	⊢ 𝐵 ∈ V
9	8	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
10		fex2	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
11	7 6 9 10	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ V )
12	7	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
13	1 2 3 4 5 11 12	tsmsval2	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑦 ) ) ) ) )