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 23714

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	⊢ 𝑋 = {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ 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 ⊢ 𝑋 = {ℎ ∈ (ℝ ↑_𝑚 𝐼) ∣ ℎ finSupp 0}
2		simprl 758	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
3	1, 2	rrxfsupp 23708	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ∈ Fin)
4		simprr 760	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
5	1, 4	rrxfsupp 23708	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ∈ Fin)
6		unfi 8580	. . . . . . . 8 ⊢ (((𝑥 supp 0) ∈ Fin ∧ (𝑦 supp 0) ∈ Fin) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
7	3, 5, 6	syl2anc 576	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
8	1, 2	rrxsuppss 23709	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
9	1, 4	rrxsuppss 23709	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
10	8, 9	unssd 4051	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
11	10	sselda 3859	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 𝑘 ∈ 𝐼)
12	1, 2	rrxf 23707	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥:𝐼⟶ℝ)
13	12	ffvelrnda 6676	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℝ)
14	1, 4	rrxf 23707	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦:𝐼⟶ℝ)
15	14	ffvelrnda 6676	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℝ)
16	13, 15	resubcld 10869	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
17	16	resqcld 13426	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
18	11, 17	syldan 582	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → (((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
19	7, 18	fsumrecl 14951	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) ∈ ℝ)
20	16	sqge0d 13427	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
21	11, 20	syldan 582	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → 0 ≤ (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
22	7, 18, 21	fsumge0 15010	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ≤ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
23	19, 22	resqrtcld 14638	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ)
24	23	ralrimivva 3142	. . . 4 ⊢ (𝐼 ∈ 𝑉 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ)
25		eqid 2779	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
26	25	fmpo 7574	. . . 4 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) ∈ ℝ ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
27	24, 26	sylib 210	. . 3 ⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ)
28		rrxmval.d	. . . . 5 ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))
29	1, 28	rrxmfval 23712	. . . 4 ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))))
30	29	feq1d 6329	. . 3 ⊢ (𝐼 ∈ 𝑉 → (𝐷:(𝑋 × 𝑋)⟶ℝ ↔ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))):(𝑋 × 𝑋)⟶ℝ))
31	27, 30	mpbird 249	. 2 ⊢ (𝐼 ∈ 𝑉 → 𝐷:(𝑋 × 𝑋)⟶ℝ)
32		sqrt00 14484	. . . . . . 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 576	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0 ↔ Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0))
34	7, 18, 21	fsum00 15013	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0))
35	16	recnd 10468	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℂ)
36		sqeq0 13301	. . . . . . . . . 10 ⊢ (((𝑥‘𝑘) − (𝑦‘𝑘)) ∈ ℂ → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ((𝑥‘𝑘) − (𝑦‘𝑘)) = 0))
37	35, 36	syl 17	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ((𝑥‘𝑘) − (𝑦‘𝑘)) = 0))
38	13	recnd 10468	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℂ)
39	15	recnd 10468	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℂ)
40	38, 39	subeq0ad 10808	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑦‘𝑘)) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
41	37, 40	bitrd 271	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
42	11, 41	syldan 582	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))) → ((((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ (𝑥‘𝑘) = (𝑦‘𝑘)))
43	42	ralbidva 3147	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
44	33, 34, 43	3bitrd 297	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
45	1, 28	rrxmval 23711	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
46	45	3expb 1100	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
47	46	eqeq1d 2781	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = 0))
48	12	ffnd 6345	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 Fn 𝐼)
49	14	ffnd 6345	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 Fn 𝐼)
50		eqfnfv 6627	. . . . . . 7 ⊢ ((𝑥 Fn 𝐼 ∧ 𝑦 Fn 𝐼) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
51	48, 49, 50	syl2anc 576	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
52		ssun1 4038	. . . . . . . . . . 11 ⊢ (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
53	52	a1i 11	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
54		simpl 475	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐼 ∈ 𝑉)
55		0red 10443	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 0 ∈ ℝ)
56	12, 53, 54, 55	suppssr 7664	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥‘𝑘) = 0)
57		ssun2 4039	. . . . . . . . . . 11 ⊢ (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0))
58	57	a1i 11	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ ((𝑥 supp 0) ∪ (𝑦 supp 0)))
59	14, 58, 54, 55	suppssr 7664	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑦‘𝑘) = 0)
60	56, 59	eqtr4d 2818	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))) → (𝑥‘𝑘) = (𝑦‘𝑘))
61	60	ralrimiva 3133	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ∀𝑘 ∈ (𝐼 ∖ ((𝑥 supp 0) ∪ (𝑦 supp 0)))(𝑥‘𝑘) = (𝑦‘𝑘))
62	10, 61	raldifeq 4322	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘) ↔ ∀𝑘 ∈ 𝐼 (𝑥‘𝑘) = (𝑦‘𝑘)))
63	51, 62	bitr4d 274	. . . . 5 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑦 ↔ ∀𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(𝑥‘𝑘) = (𝑦‘𝑘)))
64	44, 47, 63	3bitr4d 303	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
65	7	3adant2 1111	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin)
66		simp2 1117	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
67	1, 66	rrxfsupp 23708	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧 supp 0) ∈ Fin)
68		unfi 8580	. . . . . . . . . . 11 ⊢ ((((𝑥 supp 0) ∪ (𝑦 supp 0)) ∈ Fin ∧ (𝑧 supp 0) ∈ Fin) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
69	65, 67, 68	syl2anc 576	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
70	69	3expa 1098	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
71	70	an32s 639	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ∈ Fin)
72	10	adantr 473	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
73		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋)
74	1, 73	rrxsuppss 23709	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑧 supp 0) ⊆ 𝐼)
75	72, 74	unssd 4051	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
76	75	sselda 3859	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → 𝑘 ∈ 𝐼)
77	13	adantlr 702	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℝ)
78	1, 73	rrxf 23707	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → 𝑧:𝐼⟶ℝ)
79	78	ffvelrnda 6676	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑧‘𝑘) ∈ ℝ)
80	77, 79	resubcld 10869	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑥‘𝑘) − (𝑧‘𝑘)) ∈ ℝ)
81	76, 80	syldan 582	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑥‘𝑘) − (𝑧‘𝑘)) ∈ ℝ)
82	15	adantlr 702	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℝ)
83	79, 82	resubcld 10869	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((𝑧‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
84	76, 83	syldan 582	. . . . . . . 8 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((𝑧‘𝑘) − (𝑦‘𝑘)) ∈ ℝ)
85	71, 81, 84	trirn 23706	. . . . . . 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 702	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑥‘𝑘) ∈ ℂ)
87	79	recnd 10468	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑧‘𝑘) ∈ ℂ)
88	39	adantlr 702	. . . . . . . . . . . 12 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (𝑦‘𝑘) ∈ ℂ)
89	86, 87, 88	npncand 10822	. . . . . . . . . . 11 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘))) = ((𝑥‘𝑘) − (𝑦‘𝑘)))
90	89	oveq1d 6991	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → ((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
91	76, 90	syldan 582	. . . . . . . . 9 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → ((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = (((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
92	91	sumeq2dv 14920	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
93	92	fveq2d 6503	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))((((𝑥‘𝑘) − (𝑧‘𝑘)) + ((𝑧‘𝑘) − (𝑦‘𝑘)))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
94		sqsubswap 13298	. . . . . . . . . . . 12 ⊢ (((𝑥‘𝑘) ∈ ℂ ∧ (𝑧‘𝑘) ∈ ℂ) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
95	86, 87, 94	syl2anc 576	. . . . . . . . . . 11 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ 𝐼) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
96	76, 95	syldan 582	. . . . . . . . . 10 ⊢ ((((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) ∧ 𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))) → (((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = (((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
97	96	sumeq2dv 14920	. . . . . . . . 9 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
98	97	fveq2d 6503	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑧‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
99	98	oveq1d 6991	. . . . . . 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 4960	. . . . . 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 473	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
102		simp1 1116	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐼 ∈ 𝑉)
103	2	3adant2 1111	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
104	4	3adant2 1111	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
105	1, 103	rrxsuppss 23709	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 supp 0) ⊆ 𝐼)
106	1, 104	rrxsuppss 23709	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 supp 0) ⊆ 𝐼)
107	105, 106	unssd 4051	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 supp 0) ∪ (𝑦 supp 0)) ⊆ 𝐼)
108	1, 66	rrxsuppss 23709	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧 supp 0) ⊆ 𝐼)
109	107, 108	unssd 4051	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)) ⊆ 𝐼)
110		ssun1 4038	. . . . . . . . . . . 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 23713	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2))
113	112	fveq2d 6503	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
114	113	3expa 1098	. . . . . . . 8 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
115	114	an32s 639	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (√‘Σ𝑘 ∈ ((𝑥 supp 0) ∪ (𝑦 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
116	101, 115	eqtrd 2815	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑥‘𝑘) − (𝑦‘𝑘))↑2)))
117	1, 28	rrxmval 23711	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
118	117	3adant3r 1161	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧𝐷𝑥) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
119	1, 28	rrxmval 23711	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
120	119	3adant3l 1160	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑧𝐷𝑦) = (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
121	118, 120	oveq12d 6994	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
122		ssun2 4039	. . . . . . . . . . . . . 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 3868	. . . . . . . . . . . . . 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 4051	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧 supp 0) ∪ (𝑥 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
127	1, 28, 102, 66, 103, 109, 69, 126	rrxmetlem 23713	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2))
128	127	fveq2d 6503	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑥 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)))
129	57, 110	sstri 3868	. . . . . . . . . . . . . 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 4051	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧 supp 0) ∪ (𝑦 supp 0)) ⊆ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0)))
132	1, 28, 102, 66, 104, 109, 69, 131	rrxmetlem 23713	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2) = Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))
133	132	fveq2d 6503	. . . . . . . . . 10 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (√‘Σ𝑘 ∈ ((𝑧 supp 0) ∪ (𝑦 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)) = (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2)))
134	128, 133	oveq12d 6994	. . . . . . . . 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 2815	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
136	135	3expa 1098	. . . . . . 7 ⊢ (((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
137	136	an32s 639	. . . . . 6 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑥‘𝑘))↑2)) + (√‘Σ𝑘 ∈ (((𝑥 supp 0) ∪ (𝑦 supp 0)) ∪ (𝑧 supp 0))(((𝑧‘𝑘) − (𝑦‘𝑘))↑2))))
138	100, 116, 137	3brtr4d 4961	. . . . 5 ⊢ (((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
139	138	ralrimiva 3133	. . . 4 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
140	64, 139	jca 504	. . 3 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
141	140	ralrimivva 3142	. 2 ⊢ (𝐼 ∈ 𝑉 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))
142		ovex 7008	. . . 4 ⊢ (ℝ ↑_𝑚 𝐼) ∈ V
143	1, 142	rabex2 5093	. . 3 ⊢ 𝑋 ∈ V
144		ismet 22636	. . 3 ⊢ (𝑋 ∈ V → (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))))))
145	143, 144	ax-mp 5	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷:(𝑋 × 𝑋)⟶ℝ ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦) ∧ ∀𝑧 ∈ 𝑋 (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))))
146	31, 141, 145	sylanbrc 575	1 ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ∀wral 3089 {crab 3093 Vcvv 3416 ∖ cdif 3827 ∪ cun 3828 ⊆ wss 3830 class class class wbr 4929 × cxp 5405 Fn wfn 6183 ⟶wf 6184 ‘cfv 6188 (class class class)co 6976 ∈ cmpo 6978 supp csupp 7633 ↑_𝑚 cmap 8206 Fincfn 8306 finSupp cfsupp 8628 ℂcc 10333 ℝcr 10334 0cc0 10335 + caddc 10338 ≤ cle 10475 − cmin 10670 2c2 11495 ↑cexp 13244 √csqrt 14453 Σcsu 14903 distcds 16430 Metcmet 20233 ℝ^crrx 23689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-rep 5049 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 ax-inf2 8898 ax-cnex 10391 ax-resscn 10392 ax-1cn 10393 ax-icn 10394 ax-addcl 10395 ax-addrcl 10396 ax-mulcl 10397 ax-mulrcl 10398 ax-mulcom 10399 ax-addass 10400 ax-mulass 10401 ax-distr 10402 ax-i2m1 10403 ax-1ne0 10404 ax-1rid 10405 ax-rnegex 10406 ax-rrecex 10407 ax-cnre 10408 ax-pre-lttri 10409 ax-pre-lttrn 10410 ax-pre-ltadd 10411 ax-pre-mulgt0 10412 ax-pre-sup 10413 ax-addf 10414 ax-mulf 10415

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3418 df-sbc 3683 df-csb 3788 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-pss 3846 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-int 4750 df-iun 4794 df-br 4930 df-opab 4992 df-mpt 5009 df-tr 5031 df-id 5312 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-se 5367 df-we 5368 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-rn 5418 df-res 5419 df-ima 5420 df-pred 5986 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-iota 6152 df-fun 6190 df-fn 6191 df-f 6192 df-f1 6193 df-fo 6194 df-f1o 6195 df-fv 6196 df-isom 6197 df-riota 6937 df-ov 6979 df-oprab 6980 df-mpo 6981 df-of 7227 df-om 7397 df-1st 7501 df-2nd 7502 df-supp 7634 df-tpos 7695 df-wrecs 7750 df-recs 7812 df-rdg 7850 df-1o 7905 df-oadd 7909 df-er 8089 df-map 8208 df-ixp 8260 df-en 8307 df-dom 8308 df-sdom 8309 df-fin 8310 df-fsupp 8629 df-sup 8701 df-oi 8769 df-card 9162 df-pnf 10476 df-mnf 10477 df-xr 10478 df-ltxr 10479 df-le 10480 df-sub 10672 df-neg 10673 df-div 11099 df-nn 11440 df-2 11503 df-3 11504 df-4 11505 df-5 11506 df-6 11507 df-7 11508 df-8 11509 df-9 11510 df-n0 11708 df-z 11794 df-dec 11912 df-uz 12059 df-rp 12205 df-ico 12560 df-fz 12709 df-fzo 12850 df-seq 13185 df-exp 13245 df-hash 13506 df-cj 14319 df-re 14320 df-im 14321 df-sqrt 14455 df-abs 14456 df-clim 14706 df-sum 14904 df-struct 16341 df-ndx 16342 df-slot 16343 df-base 16345 df-sets 16346 df-ress 16347 df-plusg 16434 df-mulr 16435 df-starv 16436 df-sca 16437 df-vsca 16438 df-ip 16439 df-tset 16440 df-ple 16441 df-ds 16443 df-unif 16444 df-hom 16445 df-cco 16446 df-0g 16571 df-gsum 16572 df-prds 16577 df-pws 16579 df-mgm 17710 df-sgrp 17752 df-mnd 17763 df-mhm 17803 df-grp 17894 df-minusg 17895 df-sbg 17896 df-subg 18060 df-ghm 18127 df-cntz 18218 df-cmn 18668 df-abl 18669 df-mgp 18963 df-ur 18975 df-ring 19022 df-cring 19023 df-oppr 19096 df-dvdsr 19114 df-unit 19115 df-invr 19145 df-dvr 19156 df-rnghom 19190 df-drng 19227 df-field 19228 df-subrg 19256 df-staf 19338 df-srng 19339 df-lmod 19358 df-lss 19426 df-sra 19666 df-rgmod 19667 df-met 20241 df-cnfld 20248 df-refld 20451 df-dsmm 20578 df-frlm 20593 df-nm 22895 df-tng 22897 df-tcph 23476 df-rrx 23691

This theorem is referenced by: rrxdstprj1 23715 rrxmetfi 23718

W3C validator