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 24845

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 13027	. . . 4 ⊢ ℝ^* ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ^* ∈ V)
3		id 22	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^*)
4		xnegcl 13252	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ^* → -_𝑒𝑥 ∈ ℝ^*)
5		xaddcl 13278	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
6	3, 4, 5	syl2anr 597	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^)
7		xnegcl 13252	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → -_𝑒𝑦 ∈ ℝ^*)
8		xaddcl 13278	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ -_𝑒𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
9	7, 8	sylan2 593	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_𝑒 -_𝑒𝑦) ∈ ℝ^)
10	6, 9	ifcld 4577	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^)
11	10	rgen2 3197	. . . . 5 ⊢ ∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^*
12		xrsxmet.1	. . . . . . 7 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
13	12	xrsds 21445	. . . . . 6 ⊢ 𝐷 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
14	13	fmpo 8092	. . . . 5 ⊢ (∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) ∈ ℝ^* ↔ 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
15	11, 14	mpbi 230	. . . 4 ⊢ 𝐷:(ℝ^* × ℝ^)⟶ℝ^
16	15	a1i 11	. . 3 ⊢ (⊤ → 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
17		breq2 5152	. . . . . 6 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
18		breq2 5152	. . . . . 6 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦))))
19		xsubge0 13300	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
20	19	ancoms 458	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑦 +_𝑒 -_𝑒𝑥) ↔ 𝑥 ≤ 𝑦))
21	20	biimpar 477	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +_𝑒 -_𝑒𝑥))
22		xrletri 13192	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
23	22	orcanai 1004	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
24		xsubge0 13300	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑥 +_𝑒 -_𝑒𝑦) ↔ 𝑦 ≤ 𝑥))
25	24	biimpar 477	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
26	23, 25	syldan 591	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +_𝑒 -_𝑒𝑦))
27	17, 18, 21, 26	ifbothda 4569	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
28	12	xrsdsval 21446	. . . . 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 2839	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥𝐷𝑦) ∈ ℝ^)
33		0xr 11306	. . . . . 6 ⊢ 0 ∈ ℝ^*
34		xrletri3 13193	. . . . . 6 ⊢ (((𝑥𝐷𝑦) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
35	32, 33, 34	sylancl 586	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
36		simpr 484	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦)
37		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0)
38		0re 11261	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
39	37, 38	eqeltrdi 2847	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ)
40	12	xrsdsreclb 21449	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
41	40	ad4ant124 1172	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
42	39, 41	mpbid 232	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
43	42	simpld 494	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ)
44	43	recnd 11287	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ)
45	42	simprd 495	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ)
46	45	recnd 11287	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ)
47		rexsub 13272	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
48	42, 47	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_𝑒 -_𝑒𝑦) = (𝑥 − 𝑦))
49	28	eqeq1d 2737	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
50	49	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
51	50	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0)
52		xneg11 13254	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 +_𝑒 -_𝑒𝑥) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
53	6, 33, 52	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = -_𝑒0 ↔ (𝑦 +_𝑒 -_𝑒𝑥) = 0))
54		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑦 ∈ ℝ^)
55	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑥 ∈ ℝ^)
56		xnegdi 13287	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ -_𝑒𝑥 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
57	54, 55, 56	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥))
58		xnegneg 13253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ^* → -_𝑒-_𝑒𝑥 = 𝑥)
59	58	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒-_𝑒𝑥 = 𝑥)
60	59	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 -_𝑒-_𝑒𝑥) = (-_𝑒𝑦 +_𝑒 𝑥))
61	7	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_𝑒𝑦 ∈ ℝ^)
62		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑥 ∈ ℝ^)
63		xaddcom 13279	. . . . . . . . . . . . . . . . 17 ⊢ ((-_𝑒𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
64	61, 62, 63	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (-_𝑒𝑦 +_𝑒 𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
65	57, 60, 64	3eqtrd 2779	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒(𝑦 +_𝑒 -_𝑒𝑥) = (𝑥 +_𝑒 -_𝑒𝑦))
66		xneg0 13251	. . . . . . . . . . . . . . . 16 ⊢ -_𝑒0 = 0
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_𝑒0 = 0)
68	65, 67	eqeq12d 2751	. . . . . . . . . . . . . 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 2739	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
73	72	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑦 +_𝑒 -_𝑒𝑥) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
74		eqeq1 2739	. . . . . . . . . . . . . 14 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → ((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0))
75	74	bibi1d 343	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) → (((𝑥 +_𝑒 -_𝑒𝑦) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = 0 ↔ (𝑥 +_𝑒 -_𝑒𝑦) = 0)))
76	73, 75	ifboth 4570	. . . . . . . . . . . 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 2777	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0)
80	44, 46, 79	subeq0d 11626	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦)
81	36, 80	pm2.61dane 3027	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦)
82	81	ex 412	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦))
83	12	xrsdsval 21446	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
84	83	anidms 566	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)))
85		xrleid 13190	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ≤ 𝑦)
86	85	iftrued 4539	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → if(𝑦 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑦))
87		xnegid 13277	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦 +_𝑒 -_𝑒𝑦) = 0)
88	84, 86, 87	3eqtrd 2779	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = 0)
89	88	adantl 481	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = 0)
90		oveq1 7438	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦))
91	90	eqeq1d 2737	. . . . . . 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 778	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ)
97	96	leidd 11827	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦))
98		simpr 484	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥)
99	98	oveq1d 7446	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦))
100	98	oveq1d 7446	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥))
101		simpll1 1211	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ^)
102		oveq12 7440	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
103	102	anidms 566	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
104	103	eqeq1d 2737	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0))
105	104, 88	vtoclga 3577	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ^* → (𝑥𝐷𝑥) = 0)
106	101, 105	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0)
107	100, 106	eqtrd 2775	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0)
108	107	oveq1d 7446	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦)))
109	96	recnd 11287	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ)
110	109	addlidd 11460	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦))
111	108, 110	eqtr2d 2776	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
112	97, 99, 111	3brtr3d 5179	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
113		simpr 484	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦)
114	113	oveq1d 7446	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥))
115		simplrl 777	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ)
116	114, 115	eqeltrrd 2840	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ)
117	116	leidd 11827	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥))
118		simpll1 1211	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ^)
119		simpll2 1212	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ^)
120		oveq2 7439	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦))
121	90, 120	eqtr4d 2778	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
122	121	adantl 481	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
123		eqeq2 2747	. . . . . . . . . 10 ⊢ ((𝑥 +_𝑒 -_𝑒𝑦) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
124		eqeq2 2747	. . . . . . . . . 10 ⊢ ((𝑦 +_𝑒 -_𝑒𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥))))
125		xrleloe 13183	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
126	125	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
127		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
128	127	neneqd 2943	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦)
129		biorf 936	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦)))
130		orcom 870	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))
131	129, 130	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
132	128, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
133		xrltnle 11326	. . . . . . . . . . . . . . 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 4542	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑥 +_𝑒 -_𝑒𝑦))
139	135	biimpar 477	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦)
140	139	iftrued 4539	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = (𝑦 +_𝑒 -_𝑒𝑥))
141	123, 124, 138, 140	ifbothda 4569	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
142	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_𝑒 -_𝑒𝑥), (𝑥 +_𝑒 -_𝑒𝑦)))
143	12	xrsdsval 21446	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
144	143	ancoms 458	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
145	144	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_𝑒 -_𝑒𝑦), (𝑦 +_𝑒 -_𝑒𝑥)))
146	141, 142, 145	3eqtr4d 2785	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
147	122, 146	pm2.61dane 3027	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
148	118, 119, 147	syl2anc 584	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
149	113	oveq1d 7446	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦))
150	119, 88	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0)
151	149, 150	eqtrd 2775	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0)
152	114, 151	oveq12d 7449	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0))
153	116	recnd 11287	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ)
154	153	addridd 11459	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥))
155	152, 154	eqtrd 2775	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥))
156	117, 148, 155	3brtr4d 5180	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
157		simplrl 777	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ)
158		simpll3 1213	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ^)
159		simpll1 1211	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ^)
160		simprl 771	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥)
161	12	xrsdsreclb 21449	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑧 ≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
162	158, 159, 160, 161	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
163	157, 162	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))
164	163	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ)
165	164	recnd 11287	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ)
166		simplrr 778	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ)
167		simpll2 1212	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ^)
168		simprr 773	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦)
169	12	xrsdsreclb 21449	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
170	158, 167, 168, 169	syl3anc 1370	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
171	166, 170	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))
172	171	simprd 495	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ)
173	172	recnd 11287	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ)
174	163	simpld 494	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ)
175	174	recnd 11287	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ)
176	165, 173, 175	abs3difd 15496	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
177	12	xrsdsreval 21447	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
178	164, 172, 177	syl2anc 584	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
179	12	xrsdsreval 21447	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
180	163, 179	syl 17	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
181	175, 165	abssubd 15489	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧)))
182	180, 181	eqtrd 2775	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧)))
183	12	xrsdsreval 21447	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
184	171, 183	syl 17	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
185	182, 184	oveq12d 7449	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
186	176, 178, 185	3brtr4d 5180	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
187	112, 156, 186	pm2.61da2ne 3028	. . . 4 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
188	187	3adant1 1129	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
189	2, 16, 30, 95, 188	isxmet2d 24353	. 2 ⊢ (⊤ → 𝐷 ∈ (∞Met‘ℝ^*))
190	189	mptru 1544	1 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1537 ⊤wtru 1538 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 Vcvv 3478 ifcif 4531 class class class wbr 5148 × cxp 5687 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ℝcr 11152 0cc0 11153 + caddc 11156 ℝ^*cxr 11292 < clt 11293 ≤ cle 11294 − cmin 11490 -_𝑒cxne 13149 +_𝑒 cxad 13150 abscabs 15270 distcds 17307 ℝ^*_𝑠cxrs 17547 ∞Metcxmet 21367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-er 8744 df-map 8867 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9480 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12612 df-dec 12732 df-uz 12877 df-rp 13033 df-xneg 13152 df-xadd 13153 df-icc 13391 df-fz 13545 df-seq 14040 df-exp 14100 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-struct 17181 df-slot 17216 df-ndx 17228 df-base 17246 df-plusg 17311 df-mulr 17312 df-tset 17317 df-ple 17318 df-ds 17320 df-xrs 17549 df-xmet 21375

This theorem is referenced by: xrsdsre 24846 xrsblre 24847 xrsmopn 24848 metdcnlem 24872 xmetdcn2 24873 xmetdcn 24874 metdscn 24892 metdscn2 24893

W3C validator