Definition df-xrs 14880

Description: The extended real number structure. Unlike df-cnfld 18399, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 18399. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because +oo is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +oo an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with ℂ_fld when restricted to RR. (Contributed by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
df-xrs	|- RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. } u. { <. (TopSet ` ndx ) , (ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-xrs

Step	Hyp	Ref	Expression
1		cxrs 14878	. 2 class RR*s
2		cnx 14610	. . . . . 6 class ndx
3		cbs 14613	. . . . . 6 class Base
4	2, 3	cfv 5578	. . . . 5 class ( Base ` ndx )
5		cxr 9630	. . . . 5 class RR*
6	4, 5	cop 4020	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14678	. . . . . 6 class +g
8	2, 7	cfv 5578	. . . . 5 class ( +g ` ndx )
9		cxad 11326	. . . . 5 class +e
10	8, 9	cop 4020	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14679	. . . . . 6 class .r
12	2, 11	cfv 5578	. . . . 5 class ( .r ` ndx )
13		cxmu 11327	. . . . 5 class xe
14	12, 13	cop 4020	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 4018	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14684	. . . . . 6 class TopSet
17	2, 16	cfv 5578	. . . . 5 class (TopSet ` ndx )
18		cle 9632	. . . . . 6 class <_
19		cordt 14877	. . . . . 6 class ordTop
20	18, 19	cfv 5578	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 4020	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14685	. . . . . 6 class le
23	2, 22	cfv 5578	. . . . 5 class ( le ` ndx )
24	23, 18	cop 4020	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14687	. . . . . 6 class dist
26	2, 25	cfv 5578	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1382	. . . . . . . 8 class x
30	28	cv 1382	. . . . . . . 8 class y
31	29, 30, 18	wbr 4437	. . . . . . 7 wff x <_ y
32	29	cxne 11325	. . . . . . . 8 class -e x
33	30, 32, 9	co 6281	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11325	. . . . . . . 8 class -e y
35	29, 34, 9	co 6281	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3926	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6283	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 4020	. . . 4 class <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >.
39	21, 24, 38	ctp 4018	. . 3 class { <. (TopSet ` ndx ) , (ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. }
40	15, 39	cun 3459	. 2 class ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. } u. { <. (TopSet ` ndx ) , (ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )
41	1, 40	wceq 1383	1 wff RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. } u. { <. (TopSet ` ndx ) , (ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )

This definition is referenced by:  xrsstr  18410  xrsex  18411  xrsbas  18412  xrsadd  18413  xrsmul  18414  xrstset  18415  xrsle  18416  xrsds  18439