Metamath Proof Explorer

Theorem tsmscls

Description: One half of tgptsmscls , true in any commutative monoid topological space. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmscls.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmscls.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tsmscls.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmscls.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmscls.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmscls.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmscls.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
Assertion tsmscls ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ { 𝑋 } ) ⊆ ( 𝐺 tsums 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tsmscls.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmscls.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 tsmscls.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmscls.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
5 tsmscls.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmscls.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmscls.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
8 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
9 eqid ⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) = ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } )
10 1 2 8 9 4 5 6 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
11 1 2 istps ⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
12 4 11 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
13 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } )
14 8 13 9 5 tsmsfbas ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
15 fgcl ⊢ ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
16 14 15 syl ⊢ ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
17 1 8 3 5 6 tsmslem1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝐵 )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 )
19 flfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 ) → ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) = ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
20 12 16 18 19 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) = ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
21 10 20 eqtrd ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
22 7 21 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
23 flimsncls ⊢ ( 𝑋 ∈ ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ { 𝑋 } ) ⊆ ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
24 22 23 syl ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ { 𝑋 } ) ⊆ ( 𝐽 fLim ( ( 𝐵 FilMap ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ‘ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑥 ⊆ 𝑦 } ) ) ) ) )
25 24 21 sseqtrrd ⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ { 𝑋 } ) ⊆ ( 𝐺 tsums 𝐹 ) )