txmetcnp

Description: Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
	txmetcnp.4	$⊢ L = MetOpen (E)$
Assertion	txmetcnp	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to (F \in ((J \times_{t} K) CnP L) (⟨A, B⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z)))$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3		txmetcnp.4	$⊢ L = MetOpen (E)$
4		eqid	$⊢ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) = dist (toMetSp (C) \times_{𝑠} toMetSp (D))$
5		simpl1	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to C \in ∞Met (X)$
6		simpl2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to D \in ∞Met (Y)$
7	4 5 6	tmsxps	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to dist (toMetSp (C) \times_{𝑠} toMetSp (D)) \in ∞Met (X \times Y)$
8		simpl3	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to E \in ∞Met (Z)$
9		opelxpi	$⊢ (A \in X \land B \in Y) \to ⟨A, B⟩ \in (X \times Y)$
10	9	adantl	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to ⟨A, B⟩ \in (X \times Y)$
11		eqid	$⊢ MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) = MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D)))$
12	11 3	metcnp	$⊢ (dist (toMetSp (C) \times_{𝑠} toMetSp (D)) \in ∞Met (X \times Y) \land E \in ∞Met (Z) \land ⟨A, B⟩ \in (X \times Y)) \to (F \in (MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) CnP L) (⟨A, B⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z)))$
13	7 8 10 12	syl3anc	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to (F \in (MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) CnP L) (⟨A, B⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z)))$
14	4 5 6 1 2 11	tmsxpsmopn	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) = J \times_{t} K$
15	14	oveq1d	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) CnP L = (J \times_{t} K) CnP L$
16	15	fveq1d	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to (MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) CnP L) (⟨A, B⟩) = ((J \times_{t} K) CnP L) (⟨A, B⟩)$
17	16	eleq2d	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to (F \in (MetOpen (dist (toMetSp (C) \times_{𝑠} toMetSp (D))) CnP L) (⟨A, B⟩) \leftrightarrow F \in ((J \times_{t} K) CnP L) (⟨A, B⟩))$
18		oveq2	$⊢ x = ⟨u, v⟩ \to ⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x = ⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩$
19	18	breq1d	$⊢ x = ⟨u, v⟩ \to (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \leftrightarrow ⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w)$
20		df-ov	$⊢ A F B = F (⟨A, B⟩)$
21	20	oveq1i	$⊢ (A F B) E F (x) = F (⟨A, B⟩) E F (x)$
22		fveq2	$⊢ x = ⟨u, v⟩ \to F (x) = F (⟨u, v⟩)$
23		df-ov	$⊢ u F v = F (⟨u, v⟩)$
24	22 23	eqtr4di	$⊢ x = ⟨u, v⟩ \to F (x) = u F v$
25	24	oveq2d	$⊢ x = ⟨u, v⟩ \to (A F B) E F (x) = (A F B) E (u F v)$
26	21 25	eqtr3id	$⊢ x = ⟨u, v⟩ \to F (⟨A, B⟩) E F (x) = (A F B) E (u F v)$
27	26	breq1d	$⊢ x = ⟨u, v⟩ \to (F (⟨A, B⟩) E F (x) < z \leftrightarrow (A F B) E (u F v) < z)$
28	19 27	imbi12d	$⊢ x = ⟨u, v⟩ \to ((⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z) \leftrightarrow (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \to (A F B) E (u F v) < z))$
29	28	ralxp	$⊢ \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z) \leftrightarrow \forall u \in X \forall v \in Y (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \to (A F B) E (u F v) < z)$
30	5	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to C \in ∞Met (X)$
31	6	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to D \in ∞Met (Y)$
32		simpllr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to (A \in X \land B \in Y)$
33	32	simpld	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to A \in X$
34	32	simprd	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to B \in Y$
35		simprrl	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to u \in X$
36		simprrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to v \in Y$
37	4 30 31 33 34 35 36	tmsxpsval2	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to ⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ = if (A C u \leq B D v, B D v, A C u)$
38	37	breq1d	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \leftrightarrow if (A C u \leq B D v, B D v, A C u) < w)$
39		xmetcl	$⊢ (C \in ∞Met (X) \land A \in X \land u \in X) \to A C u \in ℝ^{*}$
40	30 33 35 39	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to A C u \in ℝ^{*}$
41		xmetcl	$⊢ (D \in ∞Met (Y) \land B \in Y \land v \in Y) \to B D v \in ℝ^{*}$
42	31 34 36 41	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to B D v \in ℝ^{*}$
43		rpxr	$⊢ w \in ℝ^{+} \to w \in ℝ^{*}$
44	43	ad2antrl	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to w \in ℝ^{*}$
45		xrmaxlt	$⊢ (A C u \in ℝ^{} \land B D v \in ℝ^{} \land w \in ℝ^{*}) \to (if (A C u \leq B D v, B D v, A C u) < w \leftrightarrow (A C u < w \land B D v < w))$
46	40 42 44 45	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to (if (A C u \leq B D v, B D v, A C u) < w \leftrightarrow (A C u < w \land B D v < w))$
47	38 46	bitrd	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \leftrightarrow (A C u < w \land B D v < w))$
48	47	imbi1d	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land (w \in ℝ^{+} \land (u \in X \land v \in Y))) \to ((⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \to (A F B) E (u F v) < z) \leftrightarrow ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
49	48	anassrs	$⊢ (((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land w \in ℝ^{+}) \land (u \in X \land v \in Y)) \to ((⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \to (A F B) E (u F v) < z) \leftrightarrow ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
50	49	2ralbidva	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land w \in ℝ^{+}) \to (\forall u \in X \forall v \in Y (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) ⟨u, v⟩ < w \to (A F B) E (u F v) < z) \leftrightarrow \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
51	29 50	syl5bb	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \land w \in ℝ^{+}) \to (\forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z) \leftrightarrow \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
52	51	rexbidva	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \to (\exists w \in ℝ^{+} \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z) \leftrightarrow \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
53	52	ralbidv	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \land F : X \times Y ⟶ Z) \to (\forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z) \leftrightarrow \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z))$
54	53	pm5.32da	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to ((F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall x \in (X \times Y) (⟨A, B⟩ dist (toMetSp (C) \times_{𝑠} toMetSp (D)) x < w \to F (⟨A, B⟩) E F (x) < z)) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z)))$
55	13 17 54	3bitr3d	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (A \in X \land B \in Y)) \to (F \in ((J \times_{t} K) CnP L) (⟨A, B⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((A C u < w \land B D v < w) \to (A F B) E (u F v) < z)))$

Metamath Proof Explorer

Theorem txmetcnp

Proof