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 ⊢ J = TopOpen ⁡ G
cnmpt1plusg.p ⊢ + ˙ = + G
cnmpt1plusg.g ⊢ φ → G ∈ TopMnd
cnmpt1plusg.k ⊢ φ → K ∈ TopOn ⁡ X
cnmpt1plusg.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
cnmpt1plusg.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
Assertion cnmpt1plusg ⊢ φ → x ∈ X ⟼ A + ˙ B ∈ K Cn J

Proof

Step Hyp Ref Expression
1 tgpcn.j ⊢ J = TopOpen ⁡ G
2 cnmpt1plusg.p ⊢ + ˙ = + G
3 cnmpt1plusg.g ⊢ φ → G ∈ TopMnd
4 cnmpt1plusg.k ⊢ φ → K ∈ TopOn ⁡ X
5 cnmpt1plusg.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
6 cnmpt1plusg.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
7 eqid ⊢ Base G = Base G
8 1 7 tmdtopon ⊢ G ∈ TopMnd → J ∈ TopOn ⁡ Base G
9 3 8 syl ⊢ φ → J ∈ TopOn ⁡ Base G
10 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base G ∧ x ∈ X ⟼ A ∈ K Cn J → x ∈ X ⟼ A : X ⟶ Base G
11 4 9 5 10 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Base G
12 11 fvmptelcdm ⊢ φ ∧ x ∈ X → A ∈ Base G
13 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base G ∧ x ∈ X ⟼ B ∈ K Cn J → x ∈ X ⟼ B : X ⟶ Base G
14 4 9 6 13 syl3anc ⊢ φ → x ∈ X ⟼ B : X ⟶ Base G
15 14 fvmptelcdm ⊢ φ ∧ x ∈ X → B ∈ Base G
16 eqid ⊢ + 𝑓 ⁡ G = + 𝑓 ⁡ G
17 7 2 16 plusfval ⊢ A ∈ Base G ∧ B ∈ Base G → A + 𝑓 ⁡ G B = A + ˙ B
18 12 15 17 syl2anc ⊢ φ ∧ x ∈ X → A + 𝑓 ⁡ G B = A + ˙ B
19 18 mpteq2dva ⊢ φ → x ∈ X ⟼ A + 𝑓 ⁡ G B = x ∈ X ⟼ A + ˙ B
20 1 16 tmdcn ⊢ G ∈ TopMnd → + 𝑓 ⁡ G ∈ J × t J Cn J
21 3 20 syl ⊢ φ → + 𝑓 ⁡ G ∈ J × t J Cn J
22 4 5 6 21 cnmpt12f ⊢ φ → x ∈ X ⟼ A + 𝑓 ⁡ G B ∈ K Cn J
23 19 22 eqeltrrd ⊢ φ → x ∈ X ⟼ A + ˙ B ∈ K Cn J