rrxmet - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rrxmet		Structured version Visualization version GIF version

Theorem rrxmet 25567

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.)

**Hypotheses**
Ref	Expression
rrxmval.1	⊢ 𝑋 = {ℎ ∈ (ℝ ↑_m 𝐼) ∣ ℎ finSupp 0}
rrxmval.d	⊢ 𝐷 = (dist‘(ℝ^‘𝐼))

**Assertion**
Ref	Expression
rrxmet	⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))

Distinct variable groups: ℎ,𝐼 ℎ,𝑉 Allowed substitution hints: 𝐷(ℎ) 𝑋(ℎ)

Proof of Theorem rrxmet Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rrxmval.1	. . . . . . . . 9 ⊢ 𝑋 = {ℎ ∈ (ℝ ↑_m 𝐼) ∣ ℎ finSupp 0}
2		simprl 782	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
3	1, 2	rrxfsupp 25561	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ∈ Fin)
4		simprr 784	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
5	1, 4	rrxfsupp 25561	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ∈ Fin)
6		unfi 9151	. . . . . . . 8 ⊢ (((𝑥 supp 0) ∈ Fin ∧ (𝑦 supp 0) ∈ Fin) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
7	3, 5, 6	syl2anc 595	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
8	1, 2	rrxsuppss 25562	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
9	1, 4	rrxsuppss 25562	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
10	8, 9	unssd 4145	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
11	10	sselda 3937	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 𝑘 ∈ 𝐼)
12	1, 2	rrxf 25560	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥:𝐼⟶ℝ)
13	12	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℝ)
14	1, 4	rrxf 25560	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦:𝐼⟶ℝ)
15	14	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℝ)
16	13, 15	resubcld 11637	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
17	16	resqcld 14157	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
18	11, 17	syldan 602	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → (((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
19	7, 18	fsumrecl 15781	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
20	16	sqge0d 14169	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
21	11, 20	syldan 602	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 0 ≤ (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
22	7, 18, 21	fsumge0 15843	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
23	19, 22	resqrtcld 15465	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ)
24	23	ralrimivva 3208	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ)
25		eqid 2763	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
26	25	fmpo 8061	. . . 4 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
27	24, 26	sylib 221	. . 3 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
28		rrxmval.d	. . . . 5 ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))
29	1, 28	rrxmfval 25565	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
30	29	feq1d 6687	. . 3 ⊢ (𝐼 ∈ 𝑉 → (𝐷:(𝑋 × 𝑋)⟶ℝ ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ))
31	27, 30	mpbird 260	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐷:(𝑋 × 𝑋)⟶ℝ)
32		sqrt00 15310	. . . . . . 7 ⊢ ((Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0 ↔ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0))
33	19, 22, 32	syl2anc 595	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0 ↔ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0))
34	7, 18, 21	fsum00 15846	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0))
35	16	recnd 11232	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℂ)
36		sqeq0 14152	. . . . . . . . . 10 ⊢ (((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℂ → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ((𝑥‘𝑘) − (𝑦‘𝑘)) = 0))
37	35, 36	syl 18	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ((𝑥‘𝑘) − (𝑦‘𝑘)) = 0))
38	13	recnd 11232	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℂ)
39	15	recnd 11232	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℂ)
40	38, 39	subeq0ad 11574	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑦‘𝑘)) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
41	37, 40	bitrd 282	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
42	11, 41	syldan 602	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
43	42	ralbidva 3186	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
44	33, 34, 43	3bitrd 308	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
45	1, 28	rrxmval 25564	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
46	45	3expb 1138	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
47	46	eqeq1d 2765	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0))
48	12	ffnd 6706	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 Fn 𝐼)
49	14	ffnd 6706	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 Fn 𝐼)
50		eqfnfv 7025	. . . . . . 7 ⊢ ((𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
51	48, 49, 50	syl2anc 595	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
52		ssun1 4131	. . . . . . . . . . 11 ⊢ (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
53	52	a1i 11	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
54		simpl 487	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐼 ∈ 𝑉)
55		0red 11206	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ∈ ℝ)
56	12, 53, 54, 55	suppssr 8187	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥‘𝑘) = 0)
57		ssun2 4132	. . . . . . . . . . 11 ⊢ (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
58	57	a1i 11	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
59	14, 58, 54, 55	suppssr 8187	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑦‘𝑘) = 0)
60	56, 59	eqtr4d 2801	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥‘𝑘) = (𝑦‘𝑘))
61	60	ralrimiva 3157	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ∀𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))(𝑥‘𝑘) = (𝑦‘𝑘))
62	10, 61	raldifeq 4454	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘) ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
63	51, 62	bitr4d 285	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
64	44, 47, 63	3bitr4d 314	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
65	7	3adant2 1149	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
66		simp2 1155	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
67	1, 66	rrxfsupp 25561	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧 supp 0) ∈ Fin)
68		unfi 9151	. . . . . . . . . . 11 ⊢ ((((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin ∧ (𝑧 supp 0) ∈ Fin) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
69	65, 67, 68	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
70	69	3expa 1136	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
71	70	an32s 664	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
72	10	adantr 485	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
73		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
74	1, 73	rrxsuppss 25562	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑧 supp 0) ⊆ 𝐼)
75	72, 74	unssd 4145	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
76	75	sselda 3937	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → 𝑘 ∈ 𝐼)
77	13	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℝ)
78	1, 73	rrxf 25560	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → 𝑧:𝐼⟶ℝ)
79	78	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑧‘𝑘) ∈ ℝ)
80	77, 79	resubcld 11637	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑧‘𝑘)) ∈ ℝ)
81	76, 80	syldan 602	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑥‘𝑘) − (𝑧‘𝑘)) ∈ ℝ)
82	15	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℝ)
83	79, 82	resubcld 11637	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑧‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
84	76, 83	syldan 602	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑧‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
85	71, 81, 84	trirn 25559	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2)) ≤ ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
86	38	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℂ)
87	79	recnd 11232	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑧‘𝑘) ∈ ℂ)
88	39	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℂ)
89	86, 87, 88	npncand 11588	. . . . . . . . . . 11 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘))) = ((𝑥‘𝑘) − (𝑦‘𝑘)))
90	89	oveq1d 7425	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
91	76, 90	syldan 602	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
92	91	sumeq2dv 15749	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
93	92	fveq2d 6885	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
94		sqsubswap 14149	. . . . . . . . . . . 12 ⊢ (((𝑥‘𝑘) ∈ ℂ ∧ (𝑧‘𝑘) ∈ ℂ) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
95	86, 87, 94	syl2anc 595	. . . . . . . . . . 11 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
96	76, 95	syldan 602	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
97	96	sumeq2dv 15749	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
98	97	fveq2d 6885	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
99	98	oveq1d 7425	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
100	85, 93, 99	3brtr3d 5142	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ≤ ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
101	46	adantr 485	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
102		simp1 1154	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐼 ∈ 𝑉)
103	2	3adant2 1149	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
104	4	3adant2 1149	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
105	1, 103	rrxsuppss 25562	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
106	1, 104	rrxsuppss 25562	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
107	105, 106	unssd 4145	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
108	1, 66	rrxsuppss 25562	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧 supp 0) ⊆ 𝐼)
109	107, 108	unssd 4145	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
110		ssun1 4131	. . . . . . . . . . . 12 ⊢ ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
111	110	a1i 11	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
112	1, 28, 102, 103, 104, 109, 69, 111	rrxmetlem 25566	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
113	112	fveq2d 6885	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
114	113	3expa 1136	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
115	114	an32s 664	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
116	101, 115	eqtrd 2798	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
117	1, 28	rrxmval 25564	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
118	117	3adant3r 1200	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
119	1, 28	rrxmval 25564	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
120	119	3adant3l 1199	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
121	118, 120	oveq12d 7428	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
122		ssun2 4132	. . . . . . . . . . . . . 14 ⊢ (𝑧 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
123	122	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
124	52, 110	sstri 3946	. . . . . . . . . . . . . 14 ⊢ (𝑥 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
125	124	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
126	123, 125	unssd 4145	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧 supp 0) ∪ (𝑥 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
127	1, 28, 102, 66, 103, 109, 69, 126	rrxmetlem 25566	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
128	127	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
129	57, 110	sstri 3946	. . . . . . . . . . . . . 14 ⊢ (𝑦 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))
130	129	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
131	123, 130	unssd 4145	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
132	1, 28, 102, 66, 104, 109, 69, 131	rrxmetlem 25566	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))
133	132	fveq2d 6885	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
134	128, 133	oveq12d 7428	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
135	121, 134	eqtrd 2798	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
136	135	3expa 1136	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
137	136	an32s 664	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
138	100, 116, 137	3brtr4d 5143	. . . . 5 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
139	138	ralrimiva 3157	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
140	64, 139	jca 520	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
141	140	ralrimivva 3208	. 2 ⊢ (𝐼 ∈ 𝑉 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
142		ovex 7443	. . . 4 ⊢ (ℝ ↑_m 𝐼) ∈ V
143	1, 142	rabex2 5311	. . 3 ⊢ 𝑋 ∈ V
144		ismet 24480	. . 3 ⊢ (𝑋 ∈ V → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))))
145	143, 144	ax-mp 5	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))
146	31, 141, 145	sylanbrc 594	1 ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 {crab 3416 Vcvv 3455 ∖ cdif 3902 ∪ cun 3903 ⊆ wss 3905 class class class wbr 5109 × cxp 5659 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 supp csupp 8152 ↑_m cmap 8820 Fincfn 8939 finSupp cfsupp 9317 ℂcc 11093 ℝcr 11094 0cc0 11095 + caddc 11098 ≤ cle 11239 − cmin 11436 2c2 12290 ↑cexp 14093 √csqrt 15280 Σcsu 15733 distcds 17314 Metcmet 21508 ℝ^crrx 25542

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-pre-sup 11173 ax-addf 11174 ax-mulf 11175

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-tpos 8218 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-sup 9398 df-oi 9468 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-7 12303 df-8 12304 df-9 12305 df-n0 12500 df-z 12587 df-dec 12707 df-uz 12858 df-rp 13012 df-ico 13373 df-fz 13531 df-fzo 13679 df-seq 14034 df-exp 14094 df-hash 14363 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-clim 15535 df-sum 15734 df-struct 17202 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-starv 17320 df-sca 17321 df-vsca 17322 df-ip 17323 df-tset 17324 df-ple 17325 df-ds 17327 df-unif 17328 df-hom 17329 df-cco 17330 df-0g 17489 df-gsum 17490 df-prds 17495 df-pws 17497 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-mhm 18836 df-grp 18998 df-minusg 18999 df-sbg 19000 df-subg 19184 df-ghm 19279 df-cntz 19382 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-cring 20313 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-invr 20466 df-dvr 20479 df-rhm 20550 df-subrng 20645 df-subrg 20669 df-drng 20829 df-field 20830 df-staf 20942 df-srng 20943 df-lmod 20983 df-lss 21053 df-sra 21294 df-rgmod 21295 df-met 21516 df-cnfld 21523 df-refld 21755 df-dsmm 21882 df-frlm 21897 df-nm 24739 df-tng 24741 df-tcph 25328 df-rrx 25544

This theorem is referenced by: rrxdstprj1 25568 rrxmetfi 25571

W3C validator