rrxmet

Description: Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014) (Revised by Thierry Arnoux, 30-Jun-2019)

	Ref	Expression
Hypotheses	rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
	rrxmval.d	$⊢ D = dist (msup)$
Assertion	rrxmet	$⊢ I \in V \to D \in Met (X)$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$⊢ X = \{h \in (ℝ^{I}) \| {finSupp}_{0} (h)\}$
2		rrxmval.d	$⊢ D = dist (msup)$
3		simprl	$⊢ (I \in V \land (x \in X \land y \in X)) \to x \in X$
4	1 3	rrxfsupp	$⊢ (I \in V \land (x \in X \land y \in X)) \to x supp 0 \in Fin$
5		simprr	$⊢ (I \in V \land (x \in X \land y \in X)) \to y \in X$
6	1 5	rrxfsupp	$⊢ (I \in V \land (x \in X \land y \in X)) \to y supp 0 \in Fin$
7		unfi	$⊢ (x supp 0 \in Fin \land y supp 0 \in Fin) \to {supp}_{0} (x) \cup {supp}_{0} (y) \in Fin$
8	4 6 7	syl2anc	$⊢ (I \in V \land (x \in X \land y \in X)) \to {supp}_{0} (x) \cup {supp}_{0} (y) \in Fin$
9	1 3	rrxsuppss	$⊢ (I \in V \land (x \in X \land y \in X)) \to x supp 0 \subseteq I$
10	1 5	rrxsuppss	$⊢ (I \in V \land (x \in X \land y \in X)) \to y supp 0 \subseteq I$
11	9 10	unssd	$⊢ (I \in V \land (x \in X \land y \in X)) \to {supp}_{0} (x) \cup {supp}_{0} (y) \subseteq I$
12	11	sselda	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in ({supp}_{0} (x) \cup {supp}_{0} (y))) \to k \in I$
13	1 3	rrxf	$⊢ (I \in V \land (x \in X \land y \in X)) \to x : I ⟶ ℝ$
14	13	ffvelcdmda	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to x (k) \in ℝ$
15	1 5	rrxf	$⊢ (I \in V \land (x \in X \land y \in X)) \to y : I ⟶ ℝ$
16	15	ffvelcdmda	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to y (k) \in ℝ$
17	14 16	resubcld	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to x (k) - y (k) \in ℝ$
18	17	resqcld	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to {(x (k) - y (k))}^{2} \in ℝ$
19	12 18	syldan	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in ({supp}_{0} (x) \cup {supp}_{0} (y))) \to {(x (k) - y (k))}^{2} \in ℝ$
20	8 19	fsumrecl	$⊢ (I \in V \land (x \in X \land y \in X)) \to \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} \in ℝ$
21	17	sqge0d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to 0 \leq {(x (k) - y (k))}^{2}$
22	12 21	syldan	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in ({supp}_{0} (x) \cup {supp}_{0} (y))) \to 0 \leq {(x (k) - y (k))}^{2}$
23	8 19 22	fsumge0	$⊢ (I \in V \land (x \in X \land y \in X)) \to 0 \leq \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}$
24	20 23	resqrtcld	$⊢ (I \in V \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} \in ℝ$
25	24	ralrimivva	$⊢ I \in V \to \forall x \in X \forall y \in X \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} \in ℝ$
26		eqid	$⊢ (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}})$
27	26	fmpo	$⊢ \forall x \in X \forall y \in X \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} \in ℝ \leftrightarrow (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ$
28	25 27	sylib	$⊢ I \in V \to (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ$
29	1 2	rrxmfval	$⊢ I \in V \to D = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}})$
30	29	feq1d	$⊢ I \in V \to (D : X \times X ⟶ ℝ \leftrightarrow (x \in X, y \in X ⟼ \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ)$
31	28 30	mpbird	$⊢ I \in V \to D : X \times X ⟶ ℝ$
32		sqrt00	$⊢ (\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} \in ℝ \land 0 \leq \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}) \to (\sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} = 0)$
33	20 23 32	syl2anc	$⊢ (I \in V \land (x \in X \land y \in X)) \to (\sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} = 0)$
34	8 19 22	fsum00	$⊢ (I \in V \land (x \in X \land y \in X)) \to (\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} = 0 \leftrightarrow \forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) {(x (k) - y (k))}^{2} = 0)$
35	17	recnd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to x (k) - y (k) \in ℂ$
36		sqeq0	$⊢ x (k) - y (k) \in ℂ \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) - y (k) = 0)$
37	35 36	syl	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) - y (k) = 0)$
38	14	recnd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to x (k) \in ℂ$
39	16	recnd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to y (k) \in ℂ$
40	38 39	subeq0ad	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to (x (k) - y (k) = 0 \leftrightarrow x (k) = y (k))$
41	37 40	bitrd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in I) \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) = y (k))$
42	12 41	syldan	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in ({supp}_{0} (x) \cup {supp}_{0} (y))) \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) = y (k))$
43	42	ralbidva	$⊢ (I \in V \land (x \in X \land y \in X)) \to (\forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) {(x (k) - y (k))}^{2} = 0 \leftrightarrow \forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) x (k) = y (k))$
44	33 34 43	3bitrd	$⊢ (I \in V \land (x \in X \land y \in X)) \to (\sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) x (k) = y (k))$
45	1 2	rrxmval	$⊢ (I \in V \land x \in X \land y \in X) \to x D y = \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}$
46	45	3expb	$⊢ (I \in V \land (x \in X \land y \in X)) \to x D y = \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}$
47	46	eqeq1d	$⊢ (I \in V \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = 0)$
48	13	ffnd	$⊢ (I \in V \land (x \in X \land y \in X)) \to x Fn I$
49	15	ffnd	$⊢ (I \in V \land (x \in X \land y \in X)) \to y Fn I$
50		eqfnfv	$⊢ (x Fn I \land y Fn I) \to (x = y \leftrightarrow \forall k \in I x (k) = y (k))$
51	48 49 50	syl2anc	$⊢ (I \in V \land (x \in X \land y \in X)) \to (x = y \leftrightarrow \forall k \in I x (k) = y (k))$
52		ssun1	$⊢ x supp 0 \subseteq {supp}_{0} (x) \cup {supp}_{0} (y)$
53	52	a1i	$⊢ (I \in V \land (x \in X \land y \in X)) \to x supp 0 \subseteq {supp}_{0} (x) \cup {supp}_{0} (y)$
54		simpl	$⊢ (I \in V \land (x \in X \land y \in X)) \to I \in V$
55		0red	$⊢ (I \in V \land (x \in X \land y \in X)) \to 0 \in ℝ$
56	13 53 54 55	suppssr	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in (I ∖ ({supp}_{0} (x) \cup {supp}_{0} (y)))) \to x (k) = 0$
57		ssun2	$⊢ y supp 0 \subseteq {supp}_{0} (x) \cup {supp}_{0} (y)$
58	57	a1i	$⊢ (I \in V \land (x \in X \land y \in X)) \to y supp 0 \subseteq {supp}_{0} (x) \cup {supp}_{0} (y)$
59	15 58 54 55	suppssr	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in (I ∖ ({supp}_{0} (x) \cup {supp}_{0} (y)))) \to y (k) = 0$
60	56 59	eqtr4d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land k \in (I ∖ ({supp}_{0} (x) \cup {supp}_{0} (y)))) \to x (k) = y (k)$
61	60	ralrimiva	$⊢ (I \in V \land (x \in X \land y \in X)) \to \forall k \in (I ∖ ({supp}_{0} (x) \cup {supp}_{0} (y))) x (k) = y (k)$
62	11 61	raldifeq	$⊢ (I \in V \land (x \in X \land y \in X)) \to (\forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) x (k) = y (k) \leftrightarrow \forall k \in I x (k) = y (k))$
63	51 62	bitr4d	$⊢ (I \in V \land (x \in X \land y \in X)) \to (x = y \leftrightarrow \forall k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) x (k) = y (k))$
64	44 47 63	3bitr4d	$⊢ (I \in V \land (x \in X \land y \in X)) \to (x D y = 0 \leftrightarrow x = y)$
65	8	3adant2	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to {supp}_{0} (x) \cup {supp}_{0} (y) \in Fin$
66		simp2	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z \in X$
67	1 66	rrxfsupp	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z supp 0 \in Fin$
68		unfi	$⊢ ({supp}_{0} (x) \cup {supp}_{0} (y) \in Fin \land z supp 0 \in Fin) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \in Fin$
69	65 67 68	syl2anc	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \in Fin$
70	69	3expa	$⊢ ((I \in V \land z \in X) \land (x \in X \land y \in X)) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \in Fin$
71	70	an32s	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \in Fin$
72	11	adantr	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to {supp}_{0} (x) \cup {supp}_{0} (y) \subseteq I$
73		simpr	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to z \in X$
74	1 73	rrxsuppss	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to z supp 0 \subseteq I$
75	72 74	unssd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \subseteq I$
76	75	sselda	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in (({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z))) \to k \in I$
77	14	adantlr	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) \in ℝ$
78	1 73	rrxf	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to z : I ⟶ ℝ$
79	78	ffvelcdmda	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) \in ℝ$
80	77 79	resubcld	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) - z (k) \in ℝ$
81	76 80	syldan	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in (({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z))) \to x (k) - z (k) \in ℝ$
82	16	adantlr	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to y (k) \in ℝ$
83	79 82	resubcld	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) - y (k) \in ℝ$
84	76 83	syldan	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in (({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z))) \to z (k) - y (k) \in ℝ$
85	71 81 84	trirn	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {((x (k) - z (k)) + z (k) - y (k))}^{2}} \leq \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - z (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
86	38	adantlr	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) \in ℂ$
87	79	recnd	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) \in ℂ$
88	39	adantlr	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to y (k) \in ℂ$
89	86 87 88	npncand	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to (x (k) - z (k)) + z (k) - y (k) = x (k) - y (k)$
90	89	oveq1d	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to {((x (k) - z (k)) + z (k) - y (k))}^{2} = {(x (k) - y (k))}^{2}$
91	76 90	syldan	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in (({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z))) \to {((x (k) - z (k)) + z (k) - y (k))}^{2} = {(x (k) - y (k))}^{2}$
92	91	sumeq2dv	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {((x (k) - z (k)) + z (k) - y (k))}^{2} = \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}$
93	92	fveq2d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {((x (k) - z (k)) + z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}}$
94		sqsubswap	$⊢ (x (k) \in ℂ \land z (k) \in ℂ) \to {(x (k) - z (k))}^{2} = {(z (k) - x (k))}^{2}$
95	86 87 94	syl2anc	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to {(x (k) - z (k))}^{2} = {(z (k) - x (k))}^{2}$
96	76 95	syldan	$⊢ (((I \in V \land (x \in X \land y \in X)) \land z \in X) \land k \in (({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z))) \to {(x (k) - z (k))}^{2} = {(z (k) - x (k))}^{2}$
97	96	sumeq2dv	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - z (k))}^{2} = \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}$
98	97	fveq2d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - z (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}}$
99	98	oveq1d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - z (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
100	85 93 99	3brtr3d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}} \leq \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
101	46	adantr	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to x D y = \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}}$
102		simp1	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to I \in V$
103	3	3adant2	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to x \in X$
104	5	3adant2	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to y \in X$
105	1 103	rrxsuppss	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to x supp 0 \subseteq I$
106	1 104	rrxsuppss	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to y supp 0 \subseteq I$
107	105 106	unssd	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to {supp}_{0} (x) \cup {supp}_{0} (y) \subseteq I$
108	1 66	rrxsuppss	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z supp 0 \subseteq I$
109	107 108	unssd	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z) \subseteq I$
110		ssun1	$⊢ {supp}_{0} (x) \cup {supp}_{0} (y) \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
111	110	a1i	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to {supp}_{0} (x) \cup {supp}_{0} (y) \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
112	1 2 102 103 104 109 69 111	rrxmetlem	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2} = \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}$
113	112	fveq2d	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}}$
114	113	3expa	$⊢ ((I \in V \land z \in X) \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}}$
115	114	an32s	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in {supp}_{0} (x) \cup {supp}_{0} (y)} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}}$
116	101 115	eqtrd	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to x D y = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(x (k) - y (k))}^{2}}$
117	1 2	rrxmval	$⊢ (I \in V \land z \in X \land x \in X) \to z D x = \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2}}$
118	117	3adant3r	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z D x = \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2}}$
119	1 2	rrxmval	$⊢ (I \in V \land z \in X \land y \in X) \to z D y = \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2}}$
120	119	3adant3l	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z D y = \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2}}$
121	118 120	oveq12d	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to (z D x) + (z D y) = \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2}}$
122		ssun2	$⊢ z supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
123	122	a1i	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to z supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
124	52 110	sstri	$⊢ x supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
125	124	a1i	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to x supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
126	123 125	unssd	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to {supp}_{0} (z) \cup {supp}_{0} (x) \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
127	1 2 102 66 103 109 69 126	rrxmetlem	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2} = \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}$
128	127	fveq2d	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}}$
129	57 110	sstri	$⊢ y supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
130	129	a1i	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to y supp 0 \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
131	123 130	unssd	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to {supp}_{0} (z) \cup {supp}_{0} (y) \subseteq ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)$
132	1 2 102 66 104 109 69 131	rrxmetlem	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2} = \sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}$
133	132	fveq2d	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
134	128 133	oveq12d	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (x)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in {supp}_{0} (z) \cup {supp}_{0} (y)} {(z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
135	121 134	eqtrd	$⊢ (I \in V \land z \in X \land (x \in X \land y \in X)) \to (z D x) + (z D y) = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
136	135	3expa	$⊢ ((I \in V \land z \in X) \land (x \in X \land y \in X)) \to (z D x) + (z D y) = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
137	136	an32s	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to (z D x) + (z D y) = \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in ({supp}_{0} (x) \cup {supp}_{0} (y)) \cup {supp}_{0} (z)} {(z (k) - y (k))}^{2}}$
138	100 116 137	3brtr4d	$⊢ ((I \in V \land (x \in X \land y \in X)) \land z \in X) \to x D y \leq (z D x) + (z D y)$
139	138	ralrimiva	$⊢ (I \in V \land (x \in X \land y \in X)) \to \forall z \in X x D y \leq (z D x) + (z D y)$
140	64 139	jca	$⊢ (I \in V \land (x \in X \land y \in X)) \to ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) + (z D y))$
141	140	ralrimivva	$⊢ I \in V \to \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) + (z D y))$
142		ovex	$⊢ ℝ^{I} \in V$
143	1 142	rabex2	$⊢ X \in V$
144		ismet	$⊢ X \in V \to (D \in Met (X) \leftrightarrow (D : X \times X ⟶ ℝ \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) + (z D y))))$
145	143 144	ax-mp	$⊢ D \in Met (X) \leftrightarrow (D : X \times X ⟶ ℝ \land \forall x \in X \forall y \in X ((x D y = 0 \leftrightarrow x = y) \land \forall z \in X x D y \leq (z D x) + (z D y)))$
146	31 141 145	sylanbrc	$⊢ I \in V \to D \in Met (X)$

Metamath Proof Explorer

Theorem rrxmet

Proof