vacn

Description: Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vacn.c	$⊢ C = IndMet (U)$
	vacn.j	$⊢ J = MetOpen (C)$
	vacn.g	$⊢ G = +_{v} (U)$
Assertion	vacn	$⊢ U \in NrmCVec \to G \in ((J \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		vacn.c	$⊢ C = IndMet (U)$
2		vacn.j	$⊢ J = MetOpen (C)$
3		vacn.g	$⊢ G = +_{v} (U)$
4		eqid	$⊢ BaseSet (U) = BaseSet (U)$
5	4 3	nvgf	$⊢ U \in NrmCVec \to G : BaseSet (U) \times BaseSet (U) ⟶ BaseSet (U)$
6		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
7	6	adantl	$⊢ ((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
8		simplll	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to U \in NrmCVec$
9	4 1	imsmet	$⊢ U \in NrmCVec \to C \in Met (BaseSet (U))$
10	8 9	syl	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to C \in Met (BaseSet (U))$
11		simplrl	$⊢ ((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \to x \in BaseSet (U)$
12	11	adantr	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to x \in BaseSet (U)$
13		simprl	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to z \in BaseSet (U)$
14		metcl	$⊢ (C \in Met (BaseSet (U)) \land x \in BaseSet (U) \land z \in BaseSet (U)) \to x C z \in ℝ$
15	10 12 13 14	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to x C z \in ℝ$
16		simplrr	$⊢ ((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \to y \in BaseSet (U)$
17	16	adantr	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to y \in BaseSet (U)$
18		simprr	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to w \in BaseSet (U)$
19		metcl	$⊢ (C \in Met (BaseSet (U)) \land y \in BaseSet (U) \land w \in BaseSet (U)) \to y C w \in ℝ$
20	10 17 18 19	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to y C w \in ℝ$
21		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
22	21	ad2antlr	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to r \in ℝ$
23		lt2halves	$⊢ (x C z \in ℝ \land y C w \in ℝ \land r \in ℝ) \to ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x C z) + (y C w) < r)$
24	15 20 22 23	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x C z) + (y C w) < r)$
25		eqid	$⊢ -_{v} (U) = -_{v} (U)$
26	4 25	nvmcl	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land z \in BaseSet (U)) \to x -_{v} (U) z \in BaseSet (U)$
27	8 12 13 26	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to x -_{v} (U) z \in BaseSet (U)$
28	4 25	nvmcl	$⊢ (U \in NrmCVec \land y \in BaseSet (U) \land w \in BaseSet (U)) \to y -_{v} (U) w \in BaseSet (U)$
29	8 17 18 28	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to y -_{v} (U) w \in BaseSet (U)$
30		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
31	4 3 30	nvtri	$⊢ (U \in NrmCVec \land x -_{v} (U) z \in BaseSet (U) \land y -_{v} (U) w \in BaseSet (U)) \to {norm}_{CV} (U) ((x -_{v} (U) z) G (y -_{v} (U) w)) \leq {norm}_{CV} (U) (x -_{v} (U) z) + {norm}_{CV} (U) (y -_{v} (U) w)$
32	8 27 29 31	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to {norm}_{CV} (U) ((x -_{v} (U) z) G (y -_{v} (U) w)) \leq {norm}_{CV} (U) (x -_{v} (U) z) + {norm}_{CV} (U) (y -_{v} (U) w)$
33	4 3	nvgcl	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land y \in BaseSet (U)) \to x G y \in BaseSet (U)$
34	8 12 17 33	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to x G y \in BaseSet (U)$
35	4 3	nvgcl	$⊢ (U \in NrmCVec \land z \in BaseSet (U) \land w \in BaseSet (U)) \to z G w \in BaseSet (U)$
36	8 13 18 35	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to z G w \in BaseSet (U)$
37	4 25 30 1	imsdval	$⊢ (U \in NrmCVec \land x G y \in BaseSet (U) \land z G w \in BaseSet (U)) \to (x G y) C (z G w) = {norm}_{CV} (U) ((x G y) -_{v} (U) (z G w))$
38	8 34 36 37	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) C (z G w) = {norm}_{CV} (U) ((x G y) -_{v} (U) (z G w))$
39	4 3 25	nvaddsub4	$⊢ (U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U)) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) -_{v} (U) (z G w) = (x -_{v} (U) z) G (y -_{v} (U) w)$
40	8 12 17 13 18 39	syl122anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) -_{v} (U) (z G w) = (x -_{v} (U) z) G (y -_{v} (U) w)$
41	40	fveq2d	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to {norm}_{CV} (U) ((x G y) -_{v} (U) (z G w)) = {norm}_{CV} (U) ((x -_{v} (U) z) G (y -_{v} (U) w))$
42	38 41	eqtrd	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) C (z G w) = {norm}_{CV} (U) ((x -_{v} (U) z) G (y -_{v} (U) w))$
43	4 25 30 1	imsdval	$⊢ (U \in NrmCVec \land x \in BaseSet (U) \land z \in BaseSet (U)) \to x C z = {norm}_{CV} (U) (x -_{v} (U) z)$
44	8 12 13 43	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to x C z = {norm}_{CV} (U) (x -_{v} (U) z)$
45	4 25 30 1	imsdval	$⊢ (U \in NrmCVec \land y \in BaseSet (U) \land w \in BaseSet (U)) \to y C w = {norm}_{CV} (U) (y -_{v} (U) w)$
46	8 17 18 45	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to y C w = {norm}_{CV} (U) (y -_{v} (U) w)$
47	44 46	oveq12d	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x C z) + (y C w) = {norm}_{CV} (U) (x -_{v} (U) z) + {norm}_{CV} (U) (y -_{v} (U) w)$
48	32 42 47	3brtr4d	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) C (z G w) \leq (x C z) + (y C w)$
49		metcl	$⊢ (C \in Met (BaseSet (U)) \land x G y \in BaseSet (U) \land z G w \in BaseSet (U)) \to (x G y) C (z G w) \in ℝ$
50	10 34 36 49	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x G y) C (z G w) \in ℝ$
51	15 20	readdcld	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (x C z) + (y C w) \in ℝ$
52		lelttr	$⊢ ((x G y) C (z G w) \in ℝ \land (x C z) + (y C w) \in ℝ \land r \in ℝ) \to (((x G y) C (z G w) \leq (x C z) + (y C w) \land (x C z) + (y C w) < r) \to (x G y) C (z G w) < r)$
53	50 51 22 52	syl3anc	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to (((x G y) C (z G w) \leq (x C z) + (y C w) \land (x C z) + (y C w) < r) \to (x G y) C (z G w) < r)$
54	48 53	mpand	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to ((x C z) + (y C w) < r \to (x G y) C (z G w) < r)$
55	24 54	syld	$⊢ (((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \land (z \in BaseSet (U) \land w \in BaseSet (U))) \to ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x G y) C (z G w) < r)$
56	55	ralrimivva	$⊢ ((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \to \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x G y) C (z G w) < r)$
57		breq2	$⊢ s = \frac{r}{2} \to (x C z < s \leftrightarrow x C z < \frac{r}{2})$
58		breq2	$⊢ s = \frac{r}{2} \to (y C w < s \leftrightarrow y C w < \frac{r}{2})$
59	57 58	anbi12d	$⊢ s = \frac{r}{2} \to ((x C z < s \land y C w < s) \leftrightarrow (x C z < \frac{r}{2} \land y C w < \frac{r}{2}))$
60	59	imbi1d	$⊢ s = \frac{r}{2} \to (((x C z < s \land y C w < s) \to (x G y) C (z G w) < r) \leftrightarrow ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x G y) C (z G w) < r))$
61	60	2ralbidv	$⊢ s = \frac{r}{2} \to (\forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r) \leftrightarrow \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x G y) C (z G w) < r))$
62	61	rspcev	$⊢ (\frac{r}{2} \in ℝ^{+} \land \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < \frac{r}{2} \land y C w < \frac{r}{2}) \to (x G y) C (z G w) < r)) \to \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)$
63	7 56 62	syl2anc	$⊢ ((U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \land r \in ℝ^{+}) \to \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)$
64	63	ralrimiva	$⊢ (U \in NrmCVec \land (x \in BaseSet (U) \land y \in BaseSet (U))) \to \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)$
65	64	ralrimivva	$⊢ U \in NrmCVec \to \forall x \in BaseSet (U) \forall y \in BaseSet (U) \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)$
66	4 1	imsxmet	$⊢ U \in NrmCVec \to C \in ∞Met (BaseSet (U))$
67	2 2 2	txmetcn	$⊢ (C \in ∞Met (BaseSet (U)) \land C \in ∞Met (BaseSet (U)) \land C \in ∞Met (BaseSet (U))) \to (G \in ((J \times_{t} J) Cn J) \leftrightarrow (G : BaseSet (U) \times BaseSet (U) ⟶ BaseSet (U) \land \forall x \in BaseSet (U) \forall y \in BaseSet (U) \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)))$
68	66 66 66 67	syl3anc	$⊢ U \in NrmCVec \to (G \in ((J \times_{t} J) Cn J) \leftrightarrow (G : BaseSet (U) \times BaseSet (U) ⟶ BaseSet (U) \land \forall x \in BaseSet (U) \forall y \in BaseSet (U) \forall r \in ℝ^{+} \exists s \in ℝ^{+} \forall z \in BaseSet (U) \forall w \in BaseSet (U) ((x C z < s \land y C w < s) \to (x G y) C (z G w) < r)))$
69	5 65 68	mpbir2and	$⊢ U \in NrmCVec \to G \in ((J \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem vacn

Proof