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 24646

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 12978	. . . 4 ⊢ ℝ^* ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ^* ∈ V)
3		id 22	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^*)
4		xnegcl 13199	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ^* → -_𝑒𝑥 ∈ ℝ^*)
5		xaddcl 13225	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
6	3, 4, 5	syl2anr 596	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
7		xnegcl 13199	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → -_𝑒𝑦 ∈ ℝ^*)
8		xaddcl 13225	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ -_𝑒𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
9	7, 8	sylan2 592	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
10	6, 9	ifcld 4574	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^)
11	10	rgen2 3196	. . . . 5 ⊢ ∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^*
12		xrsxmet.1	. . . . . . 7 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
13	12	xrsds 21278	. . . . . 6 ⊢ 𝐷 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
14	13	fmpo 8058	. . . . 5 ⊢ (∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^* ↔ 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
15	11, 14	mpbi 229	. . . 4 ⊢ 𝐷:(ℝ^* × ℝ^)⟶ℝ^
16	15	a1i 11	. . 3 ⊢ (⊤ → 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
17		breq2 5152	. . . . . 6 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
18		breq2 5152	. . . . . 6 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
19		xsubge0 13247	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
20	19	ancoms 458	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
21	20	biimpar 477	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +_𝑒 -_𝑒𝑥))
22		xrletri 13139	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
23	22	orcanai 1000	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
24		xsubge0 13247	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 𝑦 ≤ 𝑥))
25	24	biimpar 477	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
26	23, 25	syldan 590	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
27	17, 18, 21, 26	ifbothda 4566	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
28	12	xrsdsval 21279	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
29	27, 28	breqtrrd 5176	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ (𝑥𝐷𝑦))
30	29	adantl 481	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → 0 ≤ (𝑥𝐷𝑦))
31	29	biantrud 531	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
32	28, 10	eqeltrd 2832	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥𝐷𝑦) ∈ ℝ^)
33		0xr 11268	. . . . . 6 ⊢ 0 ∈ ℝ^*
34		xrletri3 13140	. . . . . 6 ⊢ (((𝑥𝐷𝑦) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
35	32, 33, 34	sylancl 585	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
36		simpr 484	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦)
37		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0)
38		0re 11223	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
39	37, 38	eqeltrdi 2840	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ)
40	12	xrsdsreclb 21282	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
41	40	ad4ant124 1172	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
42	39, 41	mpbid 231	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
43	42	simpld 494	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ)
44	43	recnd 11249	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ)
45	42	simprd 495	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ)
46	45	recnd 11249	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ)
47		rexsub 13219	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
48	42, 47	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
49	28	eqeq1d 2733	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
50	49	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
51	50	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
52		xneg11 13201	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
53	6, 33, 52	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
54		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑦 ∈ ℝ^)
55	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑥 ∈ ℝ^)
56		xnegdi 13234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
57	54, 55, 56	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
58		xnegneg 13200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ^* → -_𝑒-_𝑒𝑥 = 𝑥)
59	58	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒-_𝑒𝑥 = 𝑥)
60	59	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 𝑥))
61	7	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑦 ∈ ℝ^)
62		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑥 ∈ ℝ^)
63		xaddcom 13226	. . . . . . . . . . . . . . . . 17 ⊢ ((-_𝑒𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
64	61, 62, 63	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
65	57, 60, 64	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
66		xneg0 13198	. . . . . . . . . . . . . . . 16 ⊢ -_𝑒0 = 0
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒0 = 0)
68	65, 67	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
69	53, 68	bitr3d 281	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
70	69	ad2antrr 723	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
71		biidd 262	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
72		eqeq1 2735	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
73	72	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
74		eqeq1 2735	. . . . . . . . . . . . . 14 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
75	74	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
76	73, 75	ifboth 4567	. . . . . . . . . . . 12 ⊢ ((((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ∧ ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
77	70, 71, 76	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
78	51, 77	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = 0)
79	48, 78	eqtr3d 2773	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0)
80	44, 46, 79	subeq0d 11586	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦)
81	36, 80	pm2.61dane 3028	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦)
82	81	ex 412	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦))
83	12	xrsdsval 21279	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
84	83	anidms 566	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
85		xrleid 13137	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ≤ 𝑦)
86	85	iftrued 4536	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑦))
87		xnegid 13224	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦 +_𝑒 -_𝑒𝑦) = 0)
88	84, 86, 87	3eqtrd 2775	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = 0)
89	88	adantl 481	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = 0)
90		oveq1 7419	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦))
91	90	eqeq1d 2733	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑦) = 0))
92	89, 91	syl5ibrcom 246	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 = 𝑦 → (𝑥𝐷𝑦) = 0))
93	82, 92	impbid 211	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
94	31, 35, 93	3bitr2d 307	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
95	94	adantl 481	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
96		simplrr 775	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ)
97	96	leidd 11787	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦))
98		simpr 484	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥)
99	98	oveq1d 7427	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦))
100	98	oveq1d 7427	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥))
101		simpll1 1211	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ^)
102		oveq12 7421	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
103	102	anidms 566	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
104	103	eqeq1d 2733	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0))
105	104, 88	vtoclga 3566	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ^* → (𝑥𝐷𝑥) = 0)
106	101, 105	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0)
107	100, 106	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0)
108	107	oveq1d 7427	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦)))
109	96	recnd 11249	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ)
110	109	addlidd 11422	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦))
111	108, 110	eqtr2d 2772	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
112	97, 99, 111	3brtr3d 5179	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
113		simpr 484	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦)
114	113	oveq1d 7427	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥))
115		simplrl 774	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ)
116	114, 115	eqeltrrd 2833	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ)
117	116	leidd 11787	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥))
118		simpll1 1211	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ^)
119		simpll2 1212	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ^)
120		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦))
121	90, 120	eqtr4d 2774	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
122	121	adantl 481	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
123		eqeq2 2743	. . . . . . . . . 10 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
124		eqeq2 2743	. . . . . . . . . 10 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
125		xrleloe 13130	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
126	125	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
127		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
128	127	neneqd 2944	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦)
129		biorf 934	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦)))
130		orcom 867	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))
131	129, 130	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
132	128, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
133		xrltnle 11288	. . . . . . . . . . . . . . 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 4539	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦))
139	135	biimpar 477	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦)
140	139	iftrued 4536	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥))
141	123, 124, 138, 140	ifbothda 4566	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
142	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
143	12	xrsdsval 21279	. . . . . . . . . . 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 3028	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
148	118, 119, 147	syl2anc 583	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
149	113	oveq1d 7427	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦))
150	119, 88	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0)
151	149, 150	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0)
152	114, 151	oveq12d 7430	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0))
153	116	recnd 11249	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ)
154	153	addridd 11421	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥))
155	152, 154	eqtrd 2771	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥))
156	117, 148, 155	3brtr4d 5180	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
157		simplrl 774	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ)
158		simpll3 1213	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ^)
159		simpll1 1211	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ^)
160		simprl 768	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥)
161	12	xrsdsreclb 21282	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑧 ≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
162	158, 159, 160, 161	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
163	157, 162	mpbid 231	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))
164	163	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ)
165	164	recnd 11249	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ)
166		simplrr 775	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ)
167		simpll2 1212	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ^)
168		simprr 770	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦)
169	12	xrsdsreclb 21282	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
170	158, 167, 168, 169	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
171	166, 170	mpbid 231	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))
172	171	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ)
173	172	recnd 11249	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ)
174	163	simpld 494	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ)
175	174	recnd 11249	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ)
176	165, 173, 175	abs3difd 15414	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
177	12	xrsdsreval 21280	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
178	164, 172, 177	syl2anc 583	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
179	12	xrsdsreval 21280	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
180	163, 179	syl 17	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
181	175, 165	abssubd 15407	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧)))
182	180, 181	eqtrd 2771	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧)))
183	12	xrsdsreval 21280	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
184	171, 183	syl 17	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
185	182, 184	oveq12d 7430	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
186	176, 178, 185	3brtr4d 5180	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
187	112, 156, 186	pm2.61da2ne 3029	. . . 4 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
188	187	3adant1 1129	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
189	2, 16, 30, 95, 188	isxmet2d 24154	. 2 ⊢ (⊤ → 𝐷 ∈ (∞Met‘ℝ^*))
190	189	mptru 1547	1 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1086 = wceq 1540 ⊤wtru 1541 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 Vcvv 3473 ifcif 4528 class class class wbr 5148 × cxp 5674 ⟶wf 6539 ‘cfv 6543 (class class class)co 7412 ℝcr 11115 0cc0 11116 + caddc 11119 ℝ^*cxr 11254 < clt 11255 ≤ cle 11256 − cmin 11451 -_𝑒cxne 13096 +_𝑒 cxad 13097 abscabs 15188 distcds 17213 ℝ^*_𝑠cxrs 17453 ∞Metcxmet 21219

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-er 8709 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-sup 9443 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 df-8 12288 df-9 12289 df-n0 12480 df-z 12566 df-dec 12685 df-uz 12830 df-rp 12982 df-xneg 13099 df-xadd 13100 df-icc 13338 df-fz 13492 df-seq 13974 df-exp 14035 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-struct 17087 df-slot 17122 df-ndx 17134 df-base 17152 df-plusg 17217 df-mulr 17218 df-tset 17223 df-ple 17224 df-ds 17226 df-xrs 17455 df-xmet 21227

This theorem is referenced by: xrsdsre 24647 xrsblre 24648 xrsmopn 24649 metdcnlem 24673 xmetdcn2 24674 xmetdcn 24675 metdscn 24693 metdscn2 24694

W3C validator