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	$⊢ J = TopOpen (G)$
	cnmpt1plusg.p	$⊢ \underset{˙}{+} = +_{G}$
	cnmpt1plusg.g	$⊢ φ \to G \in TopMnd$
	cnmpt1plusg.k	$⊢ φ \to K \in TopOn (X)$
	cnmpt2plusg.l	$⊢ φ \to L \in TopOn (Y)$
	cnmpt2plusg.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
	cnmpt2plusg.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
Assertion	cnmpt2plusg	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{+} B) \in ((K \times_{t} L) 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		cnmpt2plusg.l	$⊢ φ \to L \in TopOn (Y)$
6		cnmpt2plusg.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
7		cnmpt2plusg.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
8		txtopon	$⊢ (K \in TopOn (X) \land L \in TopOn (Y)) \to K \times_{t} L \in TopOn (X \times Y)$
9	4 5 8	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (X \times Y)$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	1 10	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn ({Base}_{G})$
12	3 11	syl	$⊢ φ \to J \in TopOn ({Base}_{G})$
13		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{G}) \land (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
14	9 12 6 13	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
15		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
16	15	fmpo	$⊢ \forall x \in X \forall y \in Y A \in {Base}_{G} \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
17	14 16	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in {Base}_{G}$
18	17	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y A \in {Base}_{G}$
19	18	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in {Base}_{G}$
20	19	3impa	$⊢ (φ \land x \in X \land y \in Y) \to A \in {Base}_{G}$
21		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{G}) \land (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
22	9 12 7 21	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
23		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
24	23	fmpo	$⊢ \forall x \in X \forall y \in Y B \in {Base}_{G} \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
25	22 24	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in {Base}_{G}$
26	25	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y B \in {Base}_{G}$
27	26	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to B \in {Base}_{G}$
28	27	3impa	$⊢ (φ \land x \in X \land y \in Y) \to B \in {Base}_{G}$
29		eqid	$⊢ +_{𝑓} (G) = +_{𝑓} (G)$
30	10 2 29	plusfval	$⊢ (A \in {Base}_{G} \land B \in {Base}_{G}) \to A +_{𝑓} (G) B = A \underset{˙}{+} B$
31	20 28 30	syl2anc	$⊢ (φ \land x \in X \land y \in Y) \to A +_{𝑓} (G) B = A \underset{˙}{+} B$
32	31	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ A +_{𝑓} (G) B) = (x \in X, y \in Y ⟼ A \underset{˙}{+} B)$
33	1 29	tmdcn	$⊢ G \in TopMnd \to +_{𝑓} (G) \in ((J \times_{t} J) Cn J)$
34	3 33	syl	$⊢ φ \to +_{𝑓} (G) \in ((J \times_{t} J) Cn J)$
35	4 5 6 7 34	cnmpt22f	$⊢ φ \to (x \in X, y \in Y ⟼ A +_{𝑓} (G) B) \in ((K \times_{t} L) Cn J)$
36	32 35	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ A \underset{˙}{+} B) \in ((K \times_{t} L) Cn J)$

Metamath Proof Explorer

Theorem cnmpt2plusg

Proof