Definition df-xrs 14756

Description: The extended real number structure. Unlike df-cnfld 18208, 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 18208. 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 14754	. 2 class RR*s
2		cnx 14486	. . . . . 6 class ndx
3		cbs 14489	. . . . . 6 class Base
4	2, 3	cfv 5587	. . . . 5 class ( Base ` ndx )
5		cxr 9626	. . . . 5 class RR*
6	4, 5	cop 4033	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14554	. . . . . 6 class +g
8	2, 7	cfv 5587	. . . . 5 class ( +g ` ndx )
9		cxad 11315	. . . . 5 class +e
10	8, 9	cop 4033	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14555	. . . . . 6 class .r
12	2, 11	cfv 5587	. . . . 5 class ( .r ` ndx )
13		cxmu 11316	. . . . 5 class xe
14	12, 13	cop 4033	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 4031	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14560	. . . . . 6 class TopSet
17	2, 16	cfv 5587	. . . . 5 class (TopSet ` ndx )
18		cle 9628	. . . . . 6 class <_
19		cordt 14753	. . . . . 6 class ordTop
20	18, 19	cfv 5587	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 4033	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14561	. . . . . 6 class le
23	2, 22	cfv 5587	. . . . 5 class ( le ` ndx )
24	23, 18	cop 4033	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14563	. . . . . 6 class dist
26	2, 25	cfv 5587	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1378	. . . . . . . 8 class x
30	28	cv 1378	. . . . . . . 8 class y
31	29, 30, 18	wbr 4447	. . . . . . 7 wff x <_ y
32	29	cxne 11314	. . . . . . . 8 class -e x
33	30, 32, 9	co 6283	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11314	. . . . . . . 8 class -e y
35	29, 34, 9	co 6283	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3939	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6285	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 4033	. . . 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 4031	. . 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 3474	. 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 1379	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  18219  xrsex  18220  xrsbas  18221  xrsadd  18222  xrsmul  18223  xrstset  18224  xrsle  18225  xrsds  18245