xrsds

Description: The metric of the extended real number structure. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Hypothesis	xrsds.d	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
	Assertion	xrsds	⊢ 𝐷 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrsds.d	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
2		id	⊢ ( 𝑦 ∈ ℝ^* → 𝑦 ∈ ℝ^* )
3		xnegcl	⊢ ( 𝑥 ∈ ℝ^* → -_𝑒 𝑥 ∈ ℝ^* )
4		xaddcl	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -_𝑒 𝑥 ∈ ℝ^* ) → ( 𝑦 +_𝑒 -_𝑒 𝑥 ) ∈ ℝ^* )
5	2 3 4	syl2anr	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑦 +_𝑒 -_𝑒 𝑥 ) ∈ ℝ^* )
6		xnegcl	⊢ ( 𝑦 ∈ ℝ^* → -_𝑒 𝑦 ∈ ℝ^* )
7		xaddcl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ -_𝑒 𝑦 ∈ ℝ^* ) → ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ∈ ℝ^* )
8	6 7	sylan2	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ∈ ℝ^* )
9	5 8	ifcld	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ∈ ℝ^* )
10	9	rgen2	⊢ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ∈ ℝ^*
11		eqid	⊢ ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) )
12	11	fmpo	⊢ ( ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ∈ ℝ^* ↔ ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) : ( ℝ^* × ℝ^* ) ⟶ ℝ^* )
13	10 12	mpbi	⊢ ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) : ( ℝ^* × ℝ^* ) ⟶ ℝ^*
14		xrex	⊢ ℝ^* ∈ V
15	14 14	xpex	⊢ ( ℝ^* × ℝ^* ) ∈ V
16		fex2	⊢ ( ( ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) : ( ℝ^* × ℝ^* ) ⟶ ℝ^* ∧ ( ℝ^* × ℝ^* ) ∈ V ∧ ℝ^* ∈ V ) → ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) ∈ V )
17	13 15 14 16	mp3an	⊢ ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) ∈ V
18		df-xrs	⊢ ℝ^_𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ^ ⟩ , ⟨ ( +_g ‘ ndx ) , +_𝑒 ⟩ , ⟨ ( ._r ‘ ndx ) , ·_e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) ⟩ } )
19	18	odrngds	⊢ ( ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) ∈ V → ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) = ( dist ‘ ℝ^*_𝑠 ) )
20	17 19	ax-mp	⊢ ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) ) = ( dist ‘ ℝ^*_𝑠 )
21	1 20	eqtr4i	⊢ 𝐷 = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +_𝑒 -_𝑒 𝑥 ) , ( 𝑥 +_𝑒 -_𝑒 𝑦 ) ) )

Metamath Proof Explorer

Theorem xrsds

Proof