Definition df-xrs 15393

Description: The extended real number structure. Unlike df-cnfld 18964, 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 18964. 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 15391	. 2 class RR*s
2		cnx 15111	. . . . . 6 class ndx
3		cbs 15114	. . . . . 6 class Base
4	2, 3	cfv 5599	. . . . 5 class ( Base ` ndx )
5		cxr 9676	. . . . 5 class RR*
6	4, 5	cop 4003	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 15183	. . . . . 6 class +g
8	2, 7	cfv 5599	. . . . 5 class ( +g ` ndx )
9		cxad 11409	. . . . 5 class +e
10	8, 9	cop 4003	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 15184	. . . . . 6 class .r
12	2, 11	cfv 5599	. . . . 5 class ( .r ` ndx )
13		cxmu 11410	. . . . 5 class xe
14	12, 13	cop 4003	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 4001	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 15189	. . . . . 6 class TopSet
17	2, 16	cfv 5599	. . . . 5 class (TopSet ` ndx )
18		cle 9678	. . . . . 6 class <_
19		cordt 15390	. . . . . 6 class ordTop
20	18, 19	cfv 5599	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 4003	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 15190	. . . . . 6 class le
23	2, 22	cfv 5599	. . . . 5 class ( le ` ndx )
24	23, 18	cop 4003	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 15192	. . . . . 6 class dist
26	2, 25	cfv 5599	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1437	. . . . . . . 8 class x
30	28	cv 1437	. . . . . . . 8 class y
31	29, 30, 18	wbr 4421	. . . . . . 7 wff x <_ y
32	29	cxne 11408	. . . . . . . 8 class -e x
33	30, 32, 9	co 6303	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11408	. . . . . . . 8 class -e y
35	29, 34, 9	co 6303	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3910	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6305	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 4003	. . . 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 4001	. . 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 3435	. 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 1438	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  18975  xrsex  18976  xrsbas  18977  xrsadd  18978  xrsmul  18979  xrstset  18980  xrsle  18981  xrsds  19004