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

Metamath Proof Explorer

Theorem cnmpt1plusg

Description: Continuity of the group sum; analogue of cnmpt12f which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
cnmpt1plusg.p ⊢ + = ( +g ‘ 𝐺 )
cnmpt1plusg.g ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
cnmpt1plusg.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt1plusg.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
cnmpt1plusg.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
Assertion cnmpt1plusg ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 cnmpt1plusg.p ⊢ + = ( +g ‘ 𝐺 )
3 cnmpt1plusg.g ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
4 cnmpt1plusg.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
5 cnmpt1plusg.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
6 cnmpt1plusg.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 1 7 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
9 3 8 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
10 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
11 4 9 5 10 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
12 11 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
13 cnf2 ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
14 4 9 6 13 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
15 14 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
16 eqid ⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
17 7 2 16 plusfval ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) )
18 12 15 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐵 ) ) )
20 1 16 tmdcn ⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
21 3 20 syl ⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
22 4 5 6 21 cnmpt12f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
23 19 22 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + 𝐵 ) ) ∈ ( 𝐾 Cn 𝐽 ) )