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 22612

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 11829	. . . 4 ⊢ ℝ^* ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ^* ∈ V)
3		id 22	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^*)
4		xnegcl 12044	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ^* → -_𝑒𝑥 ∈ ℝ^*)
5		xaddcl 12070	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
6	3, 4, 5	syl2anr 495	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
7		xnegcl 12044	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → -_𝑒𝑦 ∈ ℝ^*)
8		xaddcl 12070	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ -_𝑒𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
9	7, 8	sylan2 491	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
10	6, 9	ifcld 4131	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^)
11	10	rgen2a 2977	. . . . 5 ⊢ ∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^*
12		xrsxmet.1	. . . . . . 7 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
13	12	xrsds 19789	. . . . . 6 ⊢ 𝐷 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
14	13	fmpt2 7237	. . . . 5 ⊢ (∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^* ↔ 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
15	11, 14	mpbi 220	. . . 4 ⊢ 𝐷:(ℝ^* × ℝ^)⟶ℝ^
16	15	a1i 11	. . 3 ⊢ (⊤ → 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
17		breq2 4657	. . . . . 6 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
18		breq2 4657	. . . . . 6 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
19		xsubge0 12091	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
20	19	ancoms 469	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
21	20	biimpar 502	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +_𝑒 -_𝑒𝑥))
22		xrletri 11984	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
23	22	orcanai 952	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
24		xsubge0 12091	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 𝑦 ≤ 𝑥))
25	24	biimpar 502	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
26	23, 25	syldan 487	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
27	17, 18, 21, 26	ifbothda 4123	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
28	12	xrsdsval 19790	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
29	27, 28	breqtrrd 4681	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ (𝑥𝐷𝑦))
30	29	adantl 482	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → 0 ≤ (𝑥𝐷𝑦))
31	29	biantrud 528	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
32	28, 10	eqeltrd 2701	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥𝐷𝑦) ∈ ℝ^)
33		0xr 10086	. . . . . 6 ⊢ 0 ∈ ℝ^*
34		xrletri3 11985	. . . . . 6 ⊢ (((𝑥𝐷𝑦) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
35	32, 33, 34	sylancl 694	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
36		simpr 477	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦)
37		simplr 792	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0)
38		0re 10040	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
39	37, 38	syl6eqel 2709	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ)
40	12	xrsdsreclb 19793	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
41	40	3expa 1265	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
42	41	adantlr 751	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
43	39, 42	mpbid 222	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
44	43	simpld 475	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ)
45	44	recnd 10068	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ)
46	43	simprd 479	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ)
47	46	recnd 10068	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ)
48		rexsub 12064	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
49	43, 48	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
50	28	eqeq1d 2624	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
51	50	biimpa 501	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
52	51	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
53		xneg11 12046	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
54	6, 33, 53	sylancl 694	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
55		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑦 ∈ ℝ^)
56	4	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑥 ∈ ℝ^)
57		xnegdi 12078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
58	55, 56, 57	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
59		xnegneg 12045	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ^* → -_𝑒-_𝑒𝑥 = 𝑥)
60	59	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒-_𝑒𝑥 = 𝑥)
61	60	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 𝑥))
62	7	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑦 ∈ ℝ^)
63		simpl 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑥 ∈ ℝ^)
64		xaddcom 12071	. . . . . . . . . . . . . . . . 17 ⊢ ((-_𝑒𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
65	62, 63, 64	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
66	58, 61, 65	3eqtrd 2660	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
67		xneg0 12043	. . . . . . . . . . . . . . . 16 ⊢ -_𝑒0 = 0
68	67	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒0 = 0)
69	66, 68	eqeq12d 2637	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
70	54, 69	bitr3d 270	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
71	70	ad2antrr 762	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
72		biidd 252	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
73		eqeq1 2626	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
74	73	bibi1d 333	. . . . . . . . . . . . 13 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
75		eqeq1 2626	. . . . . . . . . . . . . 14 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
76	75	bibi1d 333	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
77	74, 76	ifboth 4124	. . . . . . . . . . . 12 ⊢ ((((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ∧ ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
78	71, 72, 77	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0))
79	52, 78	mpbid 222	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = 0)
80	49, 79	eqtr3d 2658	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0)
81	45, 47, 80	subeq0d 10400	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦)
82	36, 81	pm2.61dane 2881	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦)
83	82	ex 450	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦))
84	12	xrsdsval 19790	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
85	84	anidms 677	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
86		xrleid 11983	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ≤ 𝑦)
87	86	iftrued 4094	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑦))
88		xnegid 12069	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦 +_𝑒 -_𝑒𝑦) = 0)
89	85, 87, 88	3eqtrd 2660	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = 0)
90	89	adantl 482	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = 0)
91		oveq1 6657	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦))
92	91	eqeq1d 2624	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑦) = 0))
93	90, 92	syl5ibrcom 237	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 = 𝑦 → (𝑥𝐷𝑦) = 0))
94	83, 93	impbid 202	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
95	31, 35, 94	3bitr2d 296	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
96	95	adantl 482	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
97		simplrr 801	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ)
98	97	leidd 10594	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦))
99		simpr 477	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥)
100	99	oveq1d 6665	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦))
101	99	oveq1d 6665	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥))
102		simpll1 1100	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ^)
103		oveq12 6659	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
104	103	anidms 677	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
105	104	eqeq1d 2624	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0))
106	105, 89	vtoclga 3272	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ^* → (𝑥𝐷𝑥) = 0)
107	102, 106	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0)
108	101, 107	eqtrd 2656	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0)
109	108	oveq1d 6665	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦)))
110	97	recnd 10068	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ)
111	110	addid2d 10237	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦))
112	109, 111	eqtr2d 2657	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
113	98, 100, 112	3brtr3d 4684	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
114		simpr 477	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦)
115	114	oveq1d 6665	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥))
116		simplrl 800	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ)
117	115, 116	eqeltrrd 2702	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ)
118	117	leidd 10594	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥))
119		simpll1 1100	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ^)
120		simpll2 1101	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ^)
121		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦))
122	91, 121	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
123	122	adantl 482	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
124		eqeq2 2633	. . . . . . . . . 10 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
125		eqeq2 2633	. . . . . . . . . 10 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
126		xrleloe 11977	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
127	126	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
128		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
129	128	neneqd 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦)
130		biorf 420	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦)))
131		orcom 402	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))
132	130, 131	syl6bb 276	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
133	129, 132	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
134		xrltnle 10105	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
135	134	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
136	127, 133, 135	3bitr2d 296	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
137	136	con2bid 344	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦 ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
138	137	biimpa 501	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → ¬ 𝑥 ≤ 𝑦)
139	138	iffalsed 4097	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦))
140	136	biimpar 502	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦)
141	140	iftrued 4094	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥))
142	124, 125, 139, 141	ifbothda 4123	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
143	28	adantr 481	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
144	12	xrsdsval 19790	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
145	144	ancoms 469	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
146	145	adantr 481	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
147	142, 143, 146	3eqtr4d 2666	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
148	123, 147	pm2.61dane 2881	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
149	119, 120, 148	syl2anc 693	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
150	114	oveq1d 6665	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦))
151	120, 89	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0)
152	150, 151	eqtrd 2656	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0)
153	115, 152	oveq12d 6668	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0))
154	117	recnd 10068	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ)
155	154	addid1d 10236	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥))
156	153, 155	eqtrd 2656	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥))
157	118, 149, 156	3brtr4d 4685	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
158		simplrl 800	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ)
159		simpll3 1102	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ^)
160		simpll1 1100	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ^)
161		simprl 794	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥)
162	12	xrsdsreclb 19793	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑧 ≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
163	159, 160, 161, 162	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
164	158, 163	mpbid 222	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))
165	164	simprd 479	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ)
166	165	recnd 10068	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ)
167		simplrr 801	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ)
168		simpll2 1101	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ^)
169		simprr 796	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦)
170	12	xrsdsreclb 19793	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
171	159, 168, 169, 170	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
172	167, 171	mpbid 222	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))
173	172	simprd 479	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ)
174	173	recnd 10068	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ)
175	164	simpld 475	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ)
176	175	recnd 10068	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ)
177	166, 174, 176	abs3difd 14199	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
178	12	xrsdsreval 19791	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
179	165, 173, 178	syl2anc 693	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
180	12	xrsdsreval 19791	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
181	164, 180	syl 17	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
182	176, 166	abssubd 14192	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧)))
183	181, 182	eqtrd 2656	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧)))
184	12	xrsdsreval 19791	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
185	172, 184	syl 17	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
186	183, 185	oveq12d 6668	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
187	177, 179, 186	3brtr4d 4685	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
188	113, 157, 187	pm2.61da2ne 2882	. . . 4 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
189	188	3adant1 1079	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
190	2, 16, 30, 96, 189	isxmet2d 22132	. 2 ⊢ (⊤ → 𝐷 ∈ (∞Met‘ℝ^*))
191	190	trud 1493	1 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ⊤wtru 1484 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 Vcvv 3200 ifcif 4086 class class class wbr 4653 × cxp 5112 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℝcr 9935 0cc0 9936 + caddc 9939 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 -_𝑒cxne 11943 +_𝑒 cxad 11944 abscabs 13974 distcds 15950 ℝ^*_𝑠cxrs 16160 ∞Metcxmt 19731

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-xneg 11946 df-xadd 11947 df-icc 12182 df-fz 12327 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-plusg 15954 df-mulr 15955 df-tset 15960 df-ple 15961 df-ds 15964 df-xrs 16162 df-xmet 19739

This theorem is referenced by: xrsdsre 22613 xrsblre 22614 xrsmopn 22615 metdcnlem 22639 xmetdcn2 22640 xmetdcn 22641 metdscn 22659 metdscn2 22660

W3C validator