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

Metamath Proof Explorer

Theorem cnmpt2plusg

Description: Continuity of the group sum; analogue of cnmpt22f 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 ‘ 𝑋 ) )
cnmpt2plusg.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
cnmpt2plusg.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
cnmpt2plusg.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
Assertion cnmpt2plusg ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 + 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 cnmpt1plusg.p ⊢ + = ( +g ‘ 𝐺 )
3 cnmpt1plusg.g ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
4 cnmpt1plusg.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
5 cnmpt2plusg.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
6 cnmpt2plusg.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
7 cnmpt2plusg.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
8 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
9 4 5 8 syl2anc ⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
10 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11 1 10 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
12 3 11 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
13 cnf2 ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
14 9 12 6 13 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
15 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
16 15 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
17 14 16 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) )
18 17 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) )
19 18 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
20 19 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
21 cnf2 ⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
22 9 12 7 21 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
23 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
24 23 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
25 22 24 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) )
26 25 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) )
27 26 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
28 27 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
29 eqid ⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
30 10 2 29 plusfval ⊢ ( ( 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) )
31 20 28 30 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 + 𝐵 ) )
32 31 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 + 𝐵 ) ) )
33 1 29 tmdcn ⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
34 3 33 syl ⊢ ( 𝜑 → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
35 4 5 6 7 34 cnmpt22f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( +𝑓 ‘ 𝐺 ) 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
36 32 35 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 + 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )