Definition df-xrs 15478

Description: The extended real number structure. Unlike df-cnfld 19048, 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 19048. 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 15476	. 2 class RR*s
2		cnx 15196	. . . . . 6 class ndx
3		cbs 15199	. . . . . 6 class Base
4	2, 3	cfv 5589	. . . . 5 class ( Base ` ndx )
5		cxr 9692	. . . . 5 class RR*
6	4, 5	cop 3965	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 15268	. . . . . 6 class +g
8	2, 7	cfv 5589	. . . . 5 class ( +g ` ndx )
9		cxad 11430	. . . . 5 class +e
10	8, 9	cop 3965	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 15269	. . . . . 6 class .r
12	2, 11	cfv 5589	. . . . 5 class ( .r ` ndx )
13		cxmu 11431	. . . . 5 class xe
14	12, 13	cop 3965	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3963	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 15274	. . . . . 6 class TopSet
17	2, 16	cfv 5589	. . . . 5 class (TopSet ` ndx )
18		cle 9694	. . . . . 6 class <_
19		cordt 15475	. . . . . 6 class ordTop
20	18, 19	cfv 5589	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3965	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 15275	. . . . . 6 class le
23	2, 22	cfv 5589	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3965	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 15277	. . . . . 6 class dist
26	2, 25	cfv 5589	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1451	. . . . . . . 8 class x
30	28	cv 1451	. . . . . . . 8 class y
31	29, 30, 18	wbr 4395	. . . . . . 7 wff x <_ y
32	29	cxne 11429	. . . . . . . 8 class -e x
33	30, 32, 9	co 6308	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11429	. . . . . . . 8 class -e y
35	29, 34, 9	co 6308	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3872	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6310	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3965	. . . 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 3963	. . 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 3388	. 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 1452	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  19059  xrsex  19060  xrsbas  19061  xrsadd  19062  xrsmul  19063  xrstset  19064  xrsle  19065  xrsds  19088