Definition df-xrs 15400

Description: The extended real number structure. Unlike df-cnfld 18971, 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 18971. 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 15398	. 2 class RR*s
2		cnx 15118	. . . . . 6 class ndx
3		cbs 15121	. . . . . 6 class Base
4	2, 3	cfv 5582	. . . . 5 class ( Base ` ndx )
5		cxr 9674	. . . . 5 class RR*
6	4, 5	cop 3974	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 15190	. . . . . 6 class +g
8	2, 7	cfv 5582	. . . . 5 class ( +g ` ndx )
9		cxad 11407	. . . . 5 class +e
10	8, 9	cop 3974	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 15191	. . . . . 6 class .r
12	2, 11	cfv 5582	. . . . 5 class ( .r ` ndx )
13		cxmu 11408	. . . . 5 class xe
14	12, 13	cop 3974	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3972	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 15196	. . . . . 6 class TopSet
17	2, 16	cfv 5582	. . . . 5 class (TopSet ` ndx )
18		cle 9676	. . . . . 6 class <_
19		cordt 15397	. . . . . 6 class ordTop
20	18, 19	cfv 5582	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3974	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 15197	. . . . . 6 class le
23	2, 22	cfv 5582	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3974	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 15199	. . . . . 6 class dist
26	2, 25	cfv 5582	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1443	. . . . . . . 8 class x
30	28	cv 1443	. . . . . . . 8 class y
31	29, 30, 18	wbr 4402	. . . . . . 7 wff x <_ y
32	29	cxne 11406	. . . . . . . 8 class -e x
33	30, 32, 9	co 6290	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11406	. . . . . . . 8 class -e y
35	29, 34, 9	co 6290	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3881	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6292	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3974	. . . 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 3972	. . 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 3402	. 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 1444	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  18982  xrsex  18983  xrsbas  18984  xrsadd  18985  xrsmul  18986  xrstset  18987  xrsle  18988  xrsds  19011