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	$⊢ \underset{˙}{+} = +_{G}$
	cnmpt1plusg.g	$⊢ φ \to G \in TopMnd$
	cnmpt1plusg.k	$⊢ φ \to K \in TopOn (X)$
	cnmpt1plusg.a	$⊢ φ \to (x \in X ⟼ A) \in (K Cn J)$
	cnmpt1plusg.b	$⊢ φ \to (x \in X ⟼ B) \in (K Cn J)$
Assertion	cnmpt1plusg	$⊢ φ \to (x \in X ⟼ A \underset{˙}{+} B) \in (K Cn J)$

Proof

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

Metamath Proof Explorer

Theorem cnmpt1plusg

Proof