Definition df-xrs 14562

Description: The extended real number structure. Unlike df-cnfld 17947, 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 17947. 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 14560	. 2 class RR*s
2		cnx 14292	. . . . . 6 class ndx
3		cbs 14295	. . . . . 6 class Base
4	2, 3	cfv 5529	. . . . 5 class ( Base ` ndx )
5		cxr 9531	. . . . 5 class RR*
6	4, 5	cop 3994	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14360	. . . . . 6 class +g
8	2, 7	cfv 5529	. . . . 5 class ( +g ` ndx )
9		cxad 11201	. . . . 5 class +e
10	8, 9	cop 3994	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14361	. . . . . 6 class .r
12	2, 11	cfv 5529	. . . . 5 class ( .r ` ndx )
13		cxmu 11202	. . . . 5 class xe
14	12, 13	cop 3994	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3992	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14366	. . . . . 6 class TopSet
17	2, 16	cfv 5529	. . . . 5 class (TopSet ` ndx )
18		cle 9533	. . . . . 6 class <_
19		cordt 14559	. . . . . 6 class ordTop
20	18, 19	cfv 5529	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3994	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14367	. . . . . 6 class le
23	2, 22	cfv 5529	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3994	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14369	. . . . . 6 class dist
26	2, 25	cfv 5529	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1369	. . . . . . . 8 class x
30	28	cv 1369	. . . . . . . 8 class y
31	29, 30, 18	wbr 4403	. . . . . . 7 wff x <_ y
32	29	cxne 11200	. . . . . . . 8 class -e x
33	30, 32, 9	co 6203	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11200	. . . . . . . 8 class -e y
35	29, 34, 9	co 6203	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3902	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6205	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3994	. . . 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 3992	. . 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 3437	. 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 1370	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  17958  xrsex  17959  xrsbas  17960  xrsadd  17961  xrsmul  17962  xrstset  17963  xrsle  17964  xrsds  17984