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 𝐽 ) )