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 25184

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 13155	. . . 4 ⊢ ℝ^* ∈ V
2	1	a1i 11	. . 3 ⊢ (⊤ → ℝ^* ∈ V)
3		id 23	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^*)
4		xnegcl 13383	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ^* → -_e𝑥 ∈ ℝ^*)
5		xaddcl 13409	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ -_e𝑥 ∈ ℝ^) → (𝑦 +_e -_e𝑥) ∈ ℝ^)
6	3, 4, 5	syl2anr 609	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑦 +_e -_e𝑥) ∈ ℝ^)
7		xnegcl 13383	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → -_e𝑦 ∈ ℝ^*)
8		xaddcl 13409	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ -_e𝑦 ∈ ℝ^) → (𝑥 +_e -_e𝑦) ∈ ℝ^)
9	7, 8	sylan2 605	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥 +_e -_e𝑦) ∈ ℝ^)
10	6, 9	ifcld 4532	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) ∈ ℝ^)
11	10	rgen2 3206	. . . . 5 ⊢ ∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) ∈ ℝ^*
12		xrsxmet.1	. . . . . . 7 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
13	12	xrsds 21768	. . . . . 6 ⊢ 𝐷 = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)))
14	13	fmpo 8114	. . . . 5 ⊢ (∀𝑥 ∈ ℝ^* ∀𝑦 ∈ ℝ^* if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) ∈ ℝ^* ↔ 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
15	11, 14	mpbi 233	. . . 4 ⊢ 𝐷:(ℝ^* × ℝ^)⟶ℝ^
16	15	a1i 11	. . 3 ⊢ (⊤ → 𝐷:(ℝ^* × ℝ^)⟶ℝ^)
17		breq2 5112	. . . . . 6 ⊢ ((𝑦 +_e -_e𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → (0 ≤ (𝑦 +_e -_e𝑥) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦))))
18		breq2 5112	. . . . . 6 ⊢ ((𝑥 +_e -_e𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → (0 ≤ (𝑥 +_e -_e𝑦) ↔ 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦))))
19		xsubge0 13431	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (0 ≤ (𝑦 +_e -_e𝑥) ↔ 𝑥 ≤ 𝑦))
20	19	ancoms 464	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑦 +_e -_e𝑥) ↔ 𝑥 ≤ 𝑦))
21	20	biimpar 483	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≤ 𝑦) → 0 ≤ (𝑦 +_e -_e𝑥))
22		xrletri 13322	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
23	22	orcanai 1018	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 𝑦 ≤ 𝑥)
24		xsubge0 13431	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (0 ≤ (𝑥 +_e -_e𝑦) ↔ 𝑦 ≤ 𝑥))
25	24	biimpar 483	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑦 ≤ 𝑥) → 0 ≤ (𝑥 +_e -_e𝑦))
26	23, 25	syldan 603	. . . . . 6 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ ¬ 𝑥 ≤ 𝑦) → 0 ≤ (𝑥 +_e -_e𝑦))
27	17, 18, 21, 26	ifbothda 4524	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)))
28	12	xrsdsval 21769	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)))
29	27, 28	breqtrrd 5139	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → 0 ≤ (𝑥𝐷𝑦))
30	29	adantl 487	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → 0 ≤ (𝑥𝐷𝑦))
31	29	biantrud 541	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
32	28, 10	eqeltrd 2864	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → (𝑥𝐷𝑦) ∈ ℝ^)
33		0xr 11395	. . . . . 6 ⊢ 0 ∈ ℝ^*
34		xrletri3 13323	. . . . . 6 ⊢ (((𝑥𝐷𝑦) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
35	32, 33, 34	sylancl 598	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
36		simpr 490	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦)
37		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = 0)
38		0re 11349	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
39	37, 38	eqeltrdi 2872	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) ∈ ℝ)
40	12	xrsdsreclb 21772	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
41	40	ad4ant124 1192	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥𝐷𝑦) ∈ ℝ ↔ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
42	39, 41	mpbid 235	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
43	42	simpld 500	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℝ)
44	43	recnd 11376	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ ℂ)
45	42	simprd 501	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℝ)
46	45	recnd 11376	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ ℂ)
47		rexsub 13403	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 +_e -_e𝑦) = (𝑥 − 𝑦))
48	42, 47	syl 18	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_e -_e𝑦) = (𝑥 − 𝑦))
49	28	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0))
50	49	biimpa 482	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0)
51	50	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0)
52		xneg11 13385	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 +_e -_e𝑥) ∈ ℝ^* ∧ 0 ∈ ℝ^*) → ( -_e(𝑦 +_e -_e𝑥) = -_e0 ↔ (𝑦 +_e -_e𝑥) = 0))
53	6, 33, 52	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ( -_e(𝑦 +_e -_e𝑥) = -_e0 ↔ (𝑦 +_e -_e𝑥) = 0))
54		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑦 ∈ ℝ^)
55	4	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_e𝑥 ∈ ℝ^)
56		xnegdi 13418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ^* ∧ -_e𝑥 ∈ ℝ^*) → -_e(𝑦 +_e -_e𝑥) = ( -_e𝑦 +_e -_e -_e𝑥))
57	54, 55, 56	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_e(𝑦 +_e -_e𝑥) = ( -_e𝑦 +_e -_e -_e𝑥))
58		xnegneg 13384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ^* → -_e -_e𝑥 = 𝑥)
59	58	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_e -_e𝑥 = 𝑥)
60	59	oveq2d 7467	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ( -_e𝑦 +_e -_e -_e𝑥) = ( -_e𝑦 +_e 𝑥))
61	7	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → -_e𝑦 ∈ ℝ^)
62		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^) → 𝑥 ∈ ℝ^)
63		xaddcom 13410	. . . . . . . . . . . . . . . . 17 ⊢ (( -_e𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → ( -_e𝑦 +_e 𝑥) = (𝑥 +_e -_e𝑦))
64	61, 62, 63	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ( -_e𝑦 +_e 𝑥) = (𝑥 +_e -_e𝑦))
65	57, 60, 64	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_e(𝑦 +_e -_e𝑥) = (𝑥 +_e -_e𝑦))
66		xneg0 13382	. . . . . . . . . . . . . . . 16 ⊢ -_e0 = 0
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → -_e0 = 0)
68	65, 67	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ( -_e(𝑦 +_e -_e𝑥) = -_e0 ↔ (𝑥 +_e -_e𝑦) = 0))
69	53, 68	bitr3d 284	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑦 +_e -_e𝑥) = 0 ↔ (𝑥 +_e -_e𝑦) = 0))
70	69	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑦 +_e -_e𝑥) = 0 ↔ (𝑥 +_e -_e𝑦) = 0))
71		biidd 265	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → ((𝑥 +_e -_e𝑦) = 0 ↔ (𝑥 +_e -_e𝑦) = 0))
72		eqeq1 2767	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +_e -_e𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → ((𝑦 +_e -_e𝑥) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0))
73	72	bibi1d 346	. . . . . . . . . . . . 13 ⊢ ((𝑦 +_e -_e𝑥) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → (((𝑦 +_e -_e𝑥) = 0 ↔ (𝑥 +_e -_e𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0 ↔ (𝑥 +_e -_e𝑦) = 0)))
74		eqeq1 2767	. . . . . . . . . . . . . 14 ⊢ ((𝑥 +_e -_e𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → ((𝑥 +_e -_e𝑦) = 0 ↔ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0))
75	74	bibi1d 346	. . . . . . . . . . . . 13 ⊢ ((𝑥 +_e -_e𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) → (((𝑥 +_e -_e𝑦) = 0 ↔ (𝑥 +_e -_e𝑦) = 0) ↔ (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0 ↔ (𝑥 +_e -_e𝑦) = 0)))
76	73, 75	ifboth 4525	. . . . . . . . . . . 12 ⊢ ((((𝑦 +_e -_e𝑥) = 0 ↔ (𝑥 +_e -_e𝑦) = 0) ∧ ((𝑥 +_e -_e𝑦) = 0 ↔ (𝑥 +_e -_e𝑦) = 0)) → (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0 ↔ (𝑥 +_e -_e𝑦) = 0))
77	70, 71, 76	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = 0 ↔ (𝑥 +_e -_e𝑦) = 0))
78	51, 77	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 +_e -_e𝑦) = 0)
79	48, 78	eqtr3d 2800	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → (𝑥 − 𝑦) = 0)
80	44, 46, 79	subeq0d 11717	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) ∧ 𝑥 ≠ 𝑦) → 𝑥 = 𝑦)
81	36, 80	pm2.61dane 3046	. . . . . . 7 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ (𝑥𝐷𝑦) = 0) → 𝑥 = 𝑦)
82	81	ex 418	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 → 𝑥 = 𝑦))
83	12	xrsdsval 21769	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_e -_e𝑦), (𝑦 +_e -_e𝑦)))
84	83	anidms 577	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = if(𝑦 ≤ 𝑦, (𝑦 +_e -_e𝑦), (𝑦 +_e -_e𝑦)))
85		xrleid 13320	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ^* → 𝑦 ≤ 𝑦)
86	85	iftrued 4493	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → if(𝑦 ≤ 𝑦, (𝑦 +_e -_e𝑦), (𝑦 +_e -_e𝑦)) = (𝑦 +_e -_e𝑦))
87		xnegid 13408	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ^* → (𝑦 +_e -_e𝑦) = 0)
88	84, 86, 87	3eqtrd 2802	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ^* → (𝑦𝐷𝑦) = 0)
89	88	adantl 487	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑦) = 0)
90		oveq1 7458	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑦))
91	90	eqeq1d 2765	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥𝐷𝑦) = 0 ↔ (𝑦𝐷𝑦) = 0))
92	89, 91	syl5ibrcom 250	. . . . . 6 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 = 𝑦 → (𝑥𝐷𝑦) = 0))
93	82, 92	impbid 215	. . . . 5 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
94	31, 35, 93	3bitr2d 310	. . . 4 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
95	94	adantl 487	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
96		simplrr 790	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℝ)
97	96	leidd 11922	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ≤ (𝑧𝐷𝑦))
98		simpr 490	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑧 = 𝑥)
99	98	oveq1d 7466	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = (𝑥𝐷𝑦))
100	98	oveq1d 7466	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = (𝑥𝐷𝑥))
101		simpll1 1231	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → 𝑥 ∈ ℝ^)
102		oveq12 7460	. . . . . . . . . . . . 13 ⊢ ((𝑦 = 𝑥 ∧ 𝑦 = 𝑥) → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
103	102	anidms 577	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦𝐷𝑦) = (𝑥𝐷𝑥))
104	103	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦𝐷𝑦) = 0 ↔ (𝑥𝐷𝑥) = 0))
105	104, 88	vtoclga 3540	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ^* → (𝑥𝐷𝑥) = 0)
106	101, 105	syl 18	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑥) = 0)
107	100, 106	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑥) = 0)
108	107	oveq1d 7466	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (0 + (𝑧𝐷𝑦)))
109	96	recnd 11376	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) ∈ ℂ)
110	109	addlidd 11550	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (0 + (𝑧𝐷𝑦)) = (𝑧𝐷𝑦))
111	108, 110	eqtr2d 2799	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑧𝐷𝑦) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
112	97, 99, 111	3brtr3d 5142	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑥) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
113		simpr 490	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑧 = 𝑦)
114	113	oveq1d 7466	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) = (𝑦𝐷𝑥))
115		simplrl 789	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑥) ∈ ℝ)
116	114, 115	eqeltrrd 2865	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℝ)
117	116	leidd 11922	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ≤ (𝑦𝐷𝑥))
118		simpll1 1231	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑥 ∈ ℝ^)
119		simpll2 1232	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → 𝑦 ∈ ℝ^)
120		oveq2 7459	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑦𝐷𝑥) = (𝑦𝐷𝑦))
121	90, 120	eqtr4d 2801	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
122	121	adantl 487	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
123		eqeq2 2775	. . . . . . . . . 10 ⊢ ((𝑥 +_e -_e𝑦) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = (𝑥 +_e -_e𝑦) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥))))
124		eqeq2 2775	. . . . . . . . . 10 ⊢ ((𝑦 +_e -_e𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)) → (if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = (𝑦 +_e -_e𝑥) ↔ if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥))))
125		xrleloe 13313	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
126	125	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
127		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦)
128	127	neneqd 2964	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑥 = 𝑦)
129		biorf 950	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 = 𝑦 ∨ 𝑥 < 𝑦)))
130		orcom 884	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑦 ∨ 𝑥 < 𝑦) ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))
131	129, 130	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 = 𝑦 → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
132	128, 131	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦)))
133		xrltnle 11415	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
134	133	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
135	126, 132, 134	3bitr2d 310	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥))
136	135	con2bid 357	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦 ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦))
137	136	biimpa 482	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → ¬ 𝑥 ≤ 𝑦)
138	137	iffalsed 4496	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = (𝑥 +_e -_e𝑦))
139	135	biimpar 483	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → 𝑥 ≤ 𝑦)
140	139	iftrued 4493	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑦 ≤ 𝑥) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = (𝑦 +_e -_e𝑥))
141	123, 124, 138, 140	ifbothda 4524	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)))
142	28	adantr 486	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = if(𝑥 ≤ 𝑦, (𝑦 +_e -_e𝑥), (𝑥 +_e -_e𝑦)))
143	12	xrsdsval 21769	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)))
144	143	ancoms 464	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)))
145	144	adantr 486	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑦𝐷𝑥) = if(𝑦 ≤ 𝑥, (𝑥 +_e -_e𝑦), (𝑦 +_e -_e𝑥)))
146	141, 142, 145	3eqtr4d 2808	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) ∧ 𝑥 ≠ 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
147	122, 146	pm2.61dane 3046	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^*) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
148	118, 119, 147	syl2anc 596	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) = (𝑦𝐷𝑥))
149	113	oveq1d 7466	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = (𝑦𝐷𝑦))
150	119, 88	syl 18	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑦) = 0)
151	149, 150	eqtrd 2798	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑧𝐷𝑦) = 0)
152	114, 151	oveq12d 7469	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑦𝐷𝑥) + 0))
153	116	recnd 11376	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑦𝐷𝑥) ∈ ℂ)
154	153	addridd 11549	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑦𝐷𝑥) + 0) = (𝑦𝐷𝑥))
155	152, 154	eqtrd 2798	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = (𝑦𝐷𝑥))
156	117, 148, 155	3brtr4d 5143	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ 𝑧 = 𝑦) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
157		simplrl 789	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) ∈ ℝ)
158		simpll3 1233	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ^)
159		simpll1 1231	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ^)
160		simprl 783	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑥)
161	12	xrsdsreclb 21772	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑧 ≠ 𝑥) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
162	158, 159, 160, 161	syl3anc 1399	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ)))
163	157, 162	mpbid 235	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ))
164	163	simprd 501	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℝ)
165	164	recnd 11376	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑥 ∈ ℂ)
166		simplrr 790	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) ∈ ℝ)
167		simpll2 1232	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ^)
168		simprr 785	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ≠ 𝑦)
169	12	xrsdsreclb 21772	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ≠ 𝑦) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
170	158, 167, 168, 169	syl3anc 1399	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑦) ∈ ℝ ↔ (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
171	166, 170	mpbid 235	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ))
172	171	simprd 501	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℝ)
173	172	recnd 11376	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑦 ∈ ℂ)
174	163	simpld 500	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℝ)
175	174	recnd 11376	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → 𝑧 ∈ ℂ)
176	165, 173, 175	abs3difd 15674	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑥 − 𝑦)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
177	12	xrsdsreval 21770	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
178	164, 172, 177	syl2anc 596	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) = (abs‘(𝑥 − 𝑦)))
179	12	xrsdsreval 21770	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
180	163, 179	syl 18	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑧 − 𝑥)))
181	175, 165	abssubd 15667	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (abs‘(𝑧 − 𝑥)) = (abs‘(𝑥 − 𝑧)))
182	180, 181	eqtrd 2798	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑥) = (abs‘(𝑥 − 𝑧)))
183	12	xrsdsreval 21770	. . . . . . . 8 ⊢ ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
184	171, 183	syl 18	. . . . . . 7 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑧𝐷𝑦) = (abs‘(𝑧 − 𝑦)))
185	182, 184	oveq12d 7469	. . . . . 6 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝑦))))
186	176, 178, 185	3brtr4d 5143	. . . . 5 ⊢ ((((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) ∧ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
187	112, 156, 186	pm2.61da2ne 3047	. . . 4 ⊢ (((𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
188	187	3adant1 1148	. . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
189	2, 16, 30, 95, 188	isxmet2d 24701	. 2 ⊢ (⊤ → 𝐷 ∈ (∞Met‘ℝ^*))
190	189	mptru 1577	1 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 Vcvv 3454 ifcif 4485 class class class wbr 5108 × cxp 5656 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ℝcr 11238 0cc0 11239 + caddc 11242 ℝ^*cxr 11381 < clt 11382 ≤ cle 11383 − cmin 11580 -_ecxne 13278 +_e cxad 13279 abscabs 15444 distcds 17481 ℝ^*_𝑠cxrs 17722 ∞Metcxmet 21714

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-sup 9471 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-rp 13161 df-xneg 13281 df-xadd 13282 df-icc 13523 df-fz 13680 df-seq 14185 df-exp 14245 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-struct 17369 df-slot 17404 df-ndx 17416 df-base 17432 df-plusg 17486 df-mulr 17487 df-tset 17492 df-ple 17493 df-ds 17495 df-xrs 17724 df-xmet 21722

This theorem is used by: xrsdsre 25185 xrsblre 25186 xrsmopn 25187 metdcnlem 25211 xmetdcn2 25212 xmetdcn 25213 metdscn 25231 metdscn2 25232

W3C validator