Definition df-xrs 15116

Description: The extended real number structure. Unlike df-cnfld 18741, 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 18741. 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 15114	. 2 class RR*s
2		cnx 14838	. . . . . 6 class ndx
3		cbs 14841	. . . . . 6 class Base
4	2, 3	cfv 5569	. . . . 5 class ( Base ` ndx )
5		cxr 9657	. . . . 5 class RR*
6	4, 5	cop 3978	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14909	. . . . . 6 class +g
8	2, 7	cfv 5569	. . . . 5 class ( +g ` ndx )
9		cxad 11369	. . . . 5 class +e
10	8, 9	cop 3978	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14910	. . . . . 6 class .r
12	2, 11	cfv 5569	. . . . 5 class ( .r ` ndx )
13		cxmu 11370	. . . . 5 class xe
14	12, 13	cop 3978	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3976	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14915	. . . . . 6 class TopSet
17	2, 16	cfv 5569	. . . . 5 class (TopSet ` ndx )
18		cle 9659	. . . . . 6 class <_
19		cordt 15113	. . . . . 6 class ordTop
20	18, 19	cfv 5569	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3978	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14916	. . . . . 6 class le
23	2, 22	cfv 5569	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3978	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14918	. . . . . 6 class dist
26	2, 25	cfv 5569	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1404	. . . . . . . 8 class x
30	28	cv 1404	. . . . . . . 8 class y
31	29, 30, 18	wbr 4395	. . . . . . 7 wff x <_ y
32	29	cxne 11368	. . . . . . . 8 class -e x
33	30, 32, 9	co 6278	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11368	. . . . . . . 8 class -e y
35	29, 34, 9	co 6278	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3885	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6280	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3978	. . . 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 3976	. . 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 3412	. 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 1405	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  18752  xrsex  18753  xrsbas  18754  xrsadd  18755  xrsmul  18756  xrstset  18757  xrsle  18758  xrsds  18781