xrsxmet - Metamath Proof Explorer

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

Theorem xrsxmet 24754

Description: The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)

**Hypothesis**
Ref	Expression
xrsxmet.1	⊢ 𝐷 = (dist‘ℝ^*_𝑠)

**Assertion**
Ref	Expression
xrsxmet	⊢ 𝐷 ∈ (∞Met‘ℝ^*)

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

Step	Hyp	Ref	Expression
1		xrex 13008	. . . 4 ⊢ ℝ^* ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ^* ∈ V)
3		id 22	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^*)
4		xnegcl 13234	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ^* → -_𝑒𝑥 ∈ ℝ^*)
5		xaddcl 13260	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
6	3, 4, 5	syl2anr 597	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
7		xnegcl 13234	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → -_𝑒𝑦 ∈ ℝ^*)
8		xaddcl 13260	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ -_𝑒𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
9	7, 8	sylan2 593	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
10	6, 9	ifcld 4552	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^)
11	10	rgen2 3185	. . . . 5 ⊢ ∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^*
12		xrsxmet.1	. . . . . . 7 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
13	12	xrsds 21382	. . . . . 6 ⊢ 𝐷 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
14	13	fmpo 8072	. . . . 5 ⊢ (∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^* ↔ 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
15	11, 14	mpbi 230	. . . 4 ⊢ 𝐷:(ℝ^* × ℝ^)⟶ℝ^
16	15	a1i 11	. . 3 ⊢ (⊤ → 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
17		breq2 5128	. . . . . 6 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
18		breq2 5128	. . . . . 6 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
19		xsubge0 13282	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
20	19	ancoms 458	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
21	20	biimpar 477	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +_𝑒 -_𝑒𝑥))
22		xrletri 13174	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
23	22	orcanai 1004	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
24		xsubge0 13282	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 𝑦 ≤ 𝑥))
25	24	biimpar 477	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
26	23, 25	syldan 591	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
27	17, 18, 21, 26	ifbothda 4544	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
28	12	xrsdsval 21383	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
29	27, 28	breqtrrd 5152	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ (𝑥𝐷𝑦))
30	29	adantl 481	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → 0 ≤ (𝑥𝐷𝑦))
31	29	biantrud 531	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
32	28, 10	eqeltrd 2835	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥𝐷𝑦) ∈ ℝ^)
33		0xr 11287	. . . . . 6 ⊢ 0 ∈ ℝ^*
34		xrletri3 13175	. . . . . 6 ⊢ (((𝑥𝐷𝑦) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
35	32, 33, 34	sylancl 586	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
36		simpr 484	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦)
37		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0)
38		0re 11242	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
39	37, 38	eqeltrdi 2843	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ)
40	12	xrsdsreclb 21386	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
41	40	ad4ant124 1174	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
42	39, 41	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
43	42	simpld 494	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ)
44	43	recnd 11268	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ)
45	42	simprd 495	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ)
46	45	recnd 11268	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ)
47		rexsub 13254	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
48	42, 47	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
49	28	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
50	49	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
51	50	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
52		xneg11 13236	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
53	6, 33, 52	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
54		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑦 ∈ ℝ^)
55	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑥 ∈ ℝ^)
56		xnegdi 13269	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
57	54, 55, 56	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
58		xnegneg 13235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ^* → -_𝑒-_𝑒𝑥 = 𝑥)
59	58	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒-_𝑒𝑥 = 𝑥)
60	59	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 𝑥))
61	7	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑦 ∈ ℝ^)
62		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑥 ∈ ℝ^)
63		xaddcom 13261	. . . . . . . . . . . . . . . . 17 ⊢ ((-_𝑒𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
64	61, 62, 63	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
65	57, 60, 64	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
66		xneg0 13233	. . . . . . . . . . . . . . . 16 ⊢ -_𝑒0 = 0
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒0 = 0)
68	65, 67	eqeq12d 2752	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
69	53, 68	bitr3d 281	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
70	69	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
71		biidd 262	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
72		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
73	72	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
74		eqeq1 2740	. . . . . . . . . . . . . 14 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
75	74	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
76	73, 75	ifboth 4545	. . . . . . . . . . . 12 ⊢ ((((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ∧ ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
77	70, 71, 76	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
78	51, 77	mpbid 232	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = 0)
79	48, 78	eqtr3d 2773	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0)
80	44, 46, 79	subeq0d 11607	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦)
81	36, 80	pm2.61dane 3020	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦)
82	81	ex 412	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦))
83	12	xrsdsval 21383	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
84	83	anidms 566	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
85		xrleid 13172	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ≤ 𝑦)
86	85	iftrued 4513	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑦))
87		xnegid 13259	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦 +_𝑒 -_𝑒𝑦) = 0)
88	84, 86, 87	3eqtrd 2775	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = 0)
89	88	adantl 481	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = 0)
90		oveq1 7417	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦))
91	90	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑦) = 0))
92	89, 91	syl5ibrcom 247	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 = 𝑦 → (𝑥𝐷𝑦) = 0))
93	82, 92	impbid 212	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
94	31, 35, 93	3bitr2d 307	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
95	94	adantl 481	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
96		simplrr 777	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ)
97	96	leidd 11808	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦))
98		simpr 484	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥)
99	98	oveq1d 7425	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦))
100	98	oveq1d 7425	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥))
101		simpll1 1213	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ^)
102		oveq12 7419	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
103	102	anidms 566	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
104	103	eqeq1d 2738	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0))
105	104, 88	vtoclga 3561	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ^* → (𝑥𝐷𝑥) = 0)
106	101, 105	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0)
107	100, 106	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0)
108	107	oveq1d 7425	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦)))
109	96	recnd 11268	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ)
110	109	addlidd 11441	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦))
111	108, 110	eqtr2d 2772	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
112	97, 99, 111	3brtr3d 5155	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
113		simpr 484	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦)
114	113	oveq1d 7425	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥))
115		simplrl 776	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ)
116	114, 115	eqeltrrd 2836	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ)
117	116	leidd 11808	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥))
118		simpll1 1213	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ^)
119		simpll2 1214	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ^)
120		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦))
121	90, 120	eqtr4d 2774	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
122	121	adantl 481	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
123		eqeq2 2748	. . . . . . . . . 10 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
124		eqeq2 2748	. . . . . . . . . 10 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
125		xrleloe 13165	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
126	125	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
127		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
128	127	neneqd 2938	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦)
129		biorf 936	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦)))
130		orcom 870	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))
131	129, 130	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
132	128, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
133		xrltnle 11307	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
134	133	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
135	126, 132, 134	3bitr2d 307	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
136	135	con2bid 354	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦 ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
137	136	biimpa 476	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → ¬ 𝑥 ≤ 𝑦)
138	137	iffalsed 4516	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦))
139	135	biimpar 477	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦)
140	139	iftrued 4513	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥))
141	123, 124, 138, 140	ifbothda 4544	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
142	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
143	12	xrsdsval 21383	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
144	143	ancoms 458	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
145	144	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
146	141, 142, 145	3eqtr4d 2781	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
147	122, 146	pm2.61dane 3020	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
148	118, 119, 147	syl2anc 584	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
149	113	oveq1d 7425	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦))
150	119, 88	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0)
151	149, 150	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0)
152	114, 151	oveq12d 7428	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0))
153	116	recnd 11268	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ)
154	153	addridd 11440	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥))
155	152, 154	eqtrd 2771	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥))
156	117, 148, 155	3brtr4d 5156	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
157		simplrl 776	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ)
158		simpll3 1215	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ^)
159		simpll1 1213	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ^)
160		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥)
161	12	xrsdsreclb 21386	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑧 ≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
162	158, 159, 160, 161	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
163	157, 162	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))
164	163	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ)
165	164	recnd 11268	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ)
166		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ)
167		simpll2 1214	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ^)
168		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦)
169	12	xrsdsreclb 21386	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
170	158, 167, 168, 169	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
171	166, 170	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))
172	171	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ)
173	172	recnd 11268	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ)
174	163	simpld 494	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ)
175	174	recnd 11268	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ)
176	165, 173, 175	abs3difd 15484	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
177	12	xrsdsreval 21384	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
178	164, 172, 177	syl2anc 584	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
179	12	xrsdsreval 21384	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
180	163, 179	syl 17	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
181	175, 165	abssubd 15477	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧)))
182	180, 181	eqtrd 2771	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧)))
183	12	xrsdsreval 21384	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
184	171, 183	syl 17	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
185	182, 184	oveq12d 7428	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
186	176, 178, 185	3brtr4d 5156	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
187	112, 156, 186	pm2.61da2ne 3021	. . . 4 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
188	187	3adant1 1130	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
189	2, 16, 30, 95, 188	isxmet2d 24271	. 2 ⊢ (⊤ → 𝐷 ∈ (∞Met‘ℝ^*))
190	189	mptru 1547	1 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ⊤wtru 1541 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 Vcvv 3464 ifcif 4505 class class class wbr 5124 × cxp 5657 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℝcr 11133 0cc0 11134 + caddc 11137 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 -_𝑒cxne 13130 +_𝑒 cxad 13131 abscabs 15258 distcds 17285 ℝ^*_𝑠cxrs 17519 ∞Metcxmet 21305

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-z 12594 df-dec 12714 df-uz 12858 df-rp 13014 df-xneg 13133 df-xadd 13134 df-icc 13374 df-fz 13530 df-seq 14025 df-exp 14085 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-struct 17171 df-slot 17206 df-ndx 17218 df-base 17234 df-plusg 17289 df-mulr 17290 df-tset 17295 df-ple 17296 df-ds 17298 df-xrs 17521 df-xmet 21313

This theorem is referenced by: xrsdsre 24755 xrsblre 24756 xrsmopn 24757 metdcnlem 24781 xmetdcn2 24782 xmetdcn 24783 metdscn 24801 metdscn2 24802

W3C validator