Theorem xrsxmet

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

	Ref	Expression
Hypothesis	xrsxmet.1	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
Assertion	xrsxmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	⊢ 𝐷 = ( dist ‘ ℝ*𝑠 )
2		xrex	⊢ ℝ* ∈ V
3	2	a1i	⊢ ( ⊤ → ℝ* ∈ V )
4		id	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ∈ ℝ* )
5		xnegcl	⊢ ( 𝑥 ∈ ℝ* → -𝑒 𝑥 ∈ ℝ* )
6		xaddcl	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑥 ∈ ℝ* ) → ( 𝑦 +𝑒 -𝑒 𝑥 ) ∈ ℝ* )
7	4 5 6	syl2anr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 +𝑒 -𝑒 𝑥 ) ∈ ℝ* )
8		xnegcl	⊢ ( 𝑦 ∈ ℝ* → -𝑒 𝑦 ∈ ℝ* )
9		xaddcl	⊢ ( ( 𝑥 ∈ ℝ* ∧ -𝑒 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) ∈ ℝ* )
10	8 9	sylan2	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) ∈ ℝ* )
11	7 10	ifcld	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ∈ ℝ* )
12	11	rgen2	⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ∈ ℝ*
13	1	xrsds	⊢ 𝐷 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
14	13	fmpo	⊢ ( ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ∈ ℝ* ↔ 𝐷 : ( ℝ* × ℝ* ) ⟶ ℝ* )
15	12 14	mpbi	⊢ 𝐷 : ( ℝ* × ℝ* ) ⟶ ℝ*
16	15	a1i	⊢ ( ⊤ → 𝐷 : ( ℝ* × ℝ* ) ⟶ ℝ* )
17		breq2	⊢ ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( 0 ≤ ( 𝑦 +𝑒 -𝑒 𝑥 ) ↔ 0 ≤ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) )
18		breq2	⊢ ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( 0 ≤ ( 𝑥 +𝑒 -𝑒 𝑦 ) ↔ 0 ≤ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) )
19		xsubge0	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 0 ≤ ( 𝑦 +𝑒 -𝑒 𝑥 ) ↔ 𝑥 ≤ 𝑦 ) )
20	19	ancoms	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 0 ≤ ( 𝑦 +𝑒 -𝑒 𝑥 ) ↔ 𝑥 ≤ 𝑦 ) )
21	20	biimpar	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≤ 𝑦 ) → 0 ≤ ( 𝑦 +𝑒 -𝑒 𝑥 ) )
22		xrletri	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
23	22	orcanai	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑥 ≤ 𝑦 ) → 𝑦 ≤ 𝑥 )
24		xsubge0	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 0 ≤ ( 𝑥 +𝑒 -𝑒 𝑦 ) ↔ 𝑦 ≤ 𝑥 ) )
25	24	biimpar	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑦 ≤ 𝑥 ) → 0 ≤ ( 𝑥 +𝑒 -𝑒 𝑦 ) )
26	23 25	syldan	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ¬ 𝑥 ≤ 𝑦 ) → 0 ≤ ( 𝑥 +𝑒 -𝑒 𝑦 ) )
27	17 18 21 26	ifbothda	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 0 ≤ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
28	1	xrsdsval	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 𝐷 𝑦 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
29	27 28	breqtrrd	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
30	29	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
31	29	biantrud	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
32	28 11	eqeltrd	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
33		0xr	⊢ 0 ∈ ℝ*
34		xrletri3	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
35	32 33 34	sylancl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
36		simpr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
37		simplr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = 0 )
38		0re	⊢ 0 ∈ ℝ
39	37 38	eqeltrdi	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
40	1	xrsdsreclb	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
41	40	ad4ant124	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ↔ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
42	39 41	mpbid	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) )
43	42	simpld	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ℝ )
44	43	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ∈ ℂ )
45	42	simprd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ℝ )
46	45	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑦 ∈ ℂ )
47		rexsub	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) = ( 𝑥 − 𝑦 ) )
48	42 47	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) = ( 𝑥 − 𝑦 ) )
49	28	eqeq1d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ) )
50	49	biimpa	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 )
51	50	adantr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 )
52		xneg11	⊢ ( ( ( 𝑦 +𝑒 -𝑒 𝑥 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = -𝑒 0 ↔ ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ) )
53	7 33 52	sylancl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = -𝑒 0 ↔ ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ) )
54		simpr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑦 ∈ ℝ* )
55	5	adantr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 𝑥 ∈ ℝ* )
56		xnegdi	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑥 ∈ ℝ* ) → -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = ( -𝑒 𝑦 +𝑒 -𝑒 -𝑒 𝑥 ) )
57	54 55 56	syl2anc	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = ( -𝑒 𝑦 +𝑒 -𝑒 -𝑒 𝑥 ) )
58		xnegneg	⊢ ( 𝑥 ∈ ℝ* → -𝑒 -𝑒 𝑥 = 𝑥 )
59	58	adantr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 -𝑒 𝑥 = 𝑥 )
60	59	oveq2d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( -𝑒 𝑦 +𝑒 -𝑒 -𝑒 𝑥 ) = ( -𝑒 𝑦 +𝑒 𝑥 ) )
61	8	adantl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 𝑦 ∈ ℝ* )
62		simpl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → 𝑥 ∈ ℝ* )
63		xaddcom	⊢ ( ( -𝑒 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( -𝑒 𝑦 +𝑒 𝑥 ) = ( 𝑥 +𝑒 -𝑒 𝑦 ) )
64	61 62 63	syl2anc	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( -𝑒 𝑦 +𝑒 𝑥 ) = ( 𝑥 +𝑒 -𝑒 𝑦 ) )
65	57 60 64	3eqtrd	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = ( 𝑥 +𝑒 -𝑒 𝑦 ) )
66		xneg0	⊢ -𝑒 0 = 0
67	66	a1i	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → -𝑒 0 = 0 )
68	65 67	eqeq12d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( -𝑒 ( 𝑦 +𝑒 -𝑒 𝑥 ) = -𝑒 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
69	53 68	bitr3d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
70	69	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
71		biidd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
72		eqeq1	⊢ ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ↔ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ) )
73	72	bibi1d	⊢ ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ↔ ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ) )
74		eqeq1	⊢ ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ↔ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ) )
75	74	bibi1d	⊢ ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) → ( ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ↔ ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ) )
76	73 75	ifboth	⊢ ( ( ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ∧ ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) ) → ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
77	70 71 76	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = 0 ↔ ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 ) )
78	51 77	mpbid	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 +𝑒 -𝑒 𝑦 ) = 0 )
79	48 78	eqtr3d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 − 𝑦 ) = 0 )
80	44 46 79	subeq0d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 = 𝑦 )
81	36 80	pm2.61dane	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ ( 𝑥 𝐷 𝑦 ) = 0 ) → 𝑥 = 𝑦 )
82	81	ex	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 → 𝑥 = 𝑦 ) )
83	1	xrsdsval	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 𝐷 𝑦 ) = if ( 𝑦 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑦 ) ) )
84	83	anidms	⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 𝐷 𝑦 ) = if ( 𝑦 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑦 ) ) )
85		xrleid	⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ 𝑦 )
86	85	iftrued	⊢ ( 𝑦 ∈ ℝ* → if ( 𝑦 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑦 ) ) = ( 𝑦 +𝑒 -𝑒 𝑦 ) )
87		xnegid	⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 +𝑒 -𝑒 𝑦 ) = 0 )
88	84 86 87	3eqtrd	⊢ ( 𝑦 ∈ ℝ* → ( 𝑦 𝐷 𝑦 ) = 0 )
89	88	adantl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 𝐷 𝑦 ) = 0 )
90		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑦 ) )
91	90	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( 𝑦 𝐷 𝑦 ) = 0 ) )
92	89 91	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 = 𝑦 → ( 𝑥 𝐷 𝑦 ) = 0 ) )
93	82 92	impbid	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
94	31 35 93	3bitr2d	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
95	94	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
96		simplrr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ )
97	96	leidd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑦 ) ≤ ( 𝑧 𝐷 𝑦 ) )
98		simpr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → 𝑧 = 𝑥 )
99	98	oveq1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
100	98	oveq1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑥 𝐷 𝑥 ) )
101		simpll1	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → 𝑥 ∈ ℝ* )
102		oveq12	⊢ ( ( 𝑦 = 𝑥 ∧ 𝑦 = 𝑥 ) → ( 𝑦 𝐷 𝑦 ) = ( 𝑥 𝐷 𝑥 ) )
103	102	anidms	⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝐷 𝑦 ) = ( 𝑥 𝐷 𝑥 ) )
104	103	eqeq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 𝐷 𝑦 ) = 0 ↔ ( 𝑥 𝐷 𝑥 ) = 0 ) )
105	104 88	vtoclga	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 𝐷 𝑥 ) = 0 )
106	101 105	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑥 𝐷 𝑥 ) = 0 )
107	100 106	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑥 ) = 0 )
108	107	oveq1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( 0 + ( 𝑧 𝐷 𝑦 ) ) )
109	96	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑦 ) ∈ ℂ )
110	109	addid2d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 0 + ( 𝑧 𝐷 𝑦 ) ) = ( 𝑧 𝐷 𝑦 ) )
111	108 110	eqtr2d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑧 𝐷 𝑦 ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
112	97 99 111	3brtr3d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑥 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
113		simpr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → 𝑧 = 𝑦 )
114	113	oveq1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑧 𝐷 𝑥 ) = ( 𝑦 𝐷 𝑥 ) )
115		simplrl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ )
116	114 115	eqeltrrd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑦 𝐷 𝑥 ) ∈ ℝ )
117	116	leidd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑦 𝐷 𝑥 ) ≤ ( 𝑦 𝐷 𝑥 ) )
118		simpll1	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → 𝑥 ∈ ℝ* )
119		simpll2	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → 𝑦 ∈ ℝ* )
120		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑦 𝐷 𝑥 ) = ( 𝑦 𝐷 𝑦 ) )
121	90 120	eqtr4d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
122	121	adantl	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
123		eqeq2	⊢ ( ( 𝑥 +𝑒 -𝑒 𝑦 ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) → ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = ( 𝑥 +𝑒 -𝑒 𝑦 ) ↔ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) ) )
124		eqeq2	⊢ ( ( 𝑦 +𝑒 -𝑒 𝑥 ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) → ( if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = ( 𝑦 +𝑒 -𝑒 𝑥 ) ↔ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) ) )
125		xrleloe	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
126	125	adantr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
127		simpr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → 𝑥 ≠ 𝑦 )
128	127	neneqd	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ¬ 𝑥 = 𝑦 )
129		biorf	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑥 < 𝑦 ↔ ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ) )
130		orcom	⊢ ( ( 𝑥 = 𝑦 ∨ 𝑥 < 𝑦 ) ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) )
131	129 130	bitrdi	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑥 < 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
132	128 131	syl	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 < 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
133		xrltnle	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
134	133	adantr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
135	126 132 134	3bitr2d	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
136	135	con2bid	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 ≤ 𝑥 ↔ ¬ 𝑥 ≤ 𝑦 ) )
137	136	biimpa	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≤ 𝑥 ) → ¬ 𝑥 ≤ 𝑦 )
138	137	iffalsed	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑦 ≤ 𝑥 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = ( 𝑥 +𝑒 -𝑒 𝑦 ) )
139	135	biimpar	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 )
140	139	iftrued	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = ( 𝑦 +𝑒 -𝑒 𝑥 ) )
141	123 124 138 140	ifbothda	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) )
142	28	adantr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
143	1	xrsdsval	⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑦 𝐷 𝑥 ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) )
144	143	ancoms	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 𝐷 𝑥 ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) )
145	144	adantr	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑦 𝐷 𝑥 ) = if ( 𝑦 ≤ 𝑥 , ( 𝑥 +𝑒 -𝑒 𝑦 ) , ( 𝑦 +𝑒 -𝑒 𝑥 ) ) )
146	141 142 145	3eqtr4d	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
147	122 146	pm2.61dane	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
148	118 119 147	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
149	113	oveq1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑧 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑦 ) )
150	119 88	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑦 𝐷 𝑦 ) = 0 )
151	149 150	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑧 𝐷 𝑦 ) = 0 )
152	114 151	oveq12d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑦 𝐷 𝑥 ) + 0 ) )
153	116	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑦 𝐷 𝑥 ) ∈ ℂ )
154	153	addid1d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( ( 𝑦 𝐷 𝑥 ) + 0 ) = ( 𝑦 𝐷 𝑥 ) )
155	152 154	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( 𝑦 𝐷 𝑥 ) )
156	117 148 155	3brtr4d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ 𝑧 = 𝑦 ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
157		simplrl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ )
158		simpll3	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑧 ∈ ℝ* )
159		simpll1	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑥 ∈ ℝ* )
160		simprl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑧 ≠ 𝑥 )
161	1	xrsdsreclb	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ≠ 𝑥 ) → ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ↔ ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) )
162	158 159 160 161	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ↔ ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) )
163	157 162	mpbid	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) )
164	163	simprd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑥 ∈ ℝ )
165	164	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑥 ∈ ℂ )
166		simplrr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ )
167		simpll2	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑦 ∈ ℝ* )
168		simprr	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑧 ≠ 𝑦 )
169	1	xrsdsreclb	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ≠ 𝑦 ) → ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ↔ ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
170	158 167 168 169	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ↔ ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
171	166 170	mpbid	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) )
172	171	simprd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑦 ∈ ℝ )
173	172	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑦 ∈ ℂ )
174	163	simpld	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑧 ∈ ℝ )
175	174	recnd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → 𝑧 ∈ ℂ )
176	165 173 175	abs3difd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( abs ‘ ( 𝑥 − 𝑧 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
177	1	xrsdsreval	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
178	164 172 177	syl2anc	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
179	1	xrsdsreval	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑧 𝐷 𝑥 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
180	163 179	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 𝐷 𝑥 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) )
181	175 165	abssubd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) )
182	180 181	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 𝐷 𝑥 ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) )
183	1	xrsdsreval	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 𝐷 𝑦 ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
184	171 183	syl	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
185	182 184	oveq12d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) + ( abs ‘ ( 𝑧 − 𝑦 ) ) ) )
186	176 178 185	3brtr4d	⊢ ( ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) ∧ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
187	112 156 186	pm2.61da2ne	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
188	187	3adant1	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
189	3 16 30 95 188	isxmet2d	⊢ ( ⊤ → 𝐷 ∈ ( ∞Met ‘ ℝ* ) )
190	189	mptru	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ* )