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 fvmptelrn ( ( 𝜑𝑥𝑋 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
13 cnf2 ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥𝑋𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥𝑋𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
14 4 9 6 13 syl3anc ( 𝜑 → ( 𝑥𝑋𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) )
15 14 fvmptelrn ( ( 𝜑𝑥𝑋 ) → 𝐵 ∈ ( 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 𝐽 ) )