Definition df-xrs 14432

Description: The extended real number structure. Unlike df-cnfld 17794, 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 17794. 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 14430	. 2 class RR*s
2		cnx 14163	. . . . . 6 class ndx
3		cbs 14166	. . . . . 6 class Base
4	2, 3	cfv 5413	. . . . 5 class ( Base ` ndx )
5		cxr 9409	. . . . 5 class RR*
6	4, 5	cop 3878	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14230	. . . . . 6 class +g
8	2, 7	cfv 5413	. . . . 5 class ( +g ` ndx )
9		cxad 11079	. . . . 5 class +e
10	8, 9	cop 3878	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14231	. . . . . 6 class .r
12	2, 11	cfv 5413	. . . . 5 class ( .r ` ndx )
13		cxmu 11080	. . . . 5 class xe
14	12, 13	cop 3878	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3876	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14236	. . . . . 6 class TopSet
17	2, 16	cfv 5413	. . . . 5 class (TopSet ` ndx )
18		cle 9411	. . . . . 6 class <_
19		cordt 14429	. . . . . 6 class ordTop
20	18, 19	cfv 5413	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3878	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14237	. . . . . 6 class le
23	2, 22	cfv 5413	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3878	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14239	. . . . . 6 class dist
26	2, 25	cfv 5413	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1368	. . . . . . . 8 class x
30	28	cv 1368	. . . . . . . 8 class y
31	29, 30, 18	wbr 4287	. . . . . . 7 wff x <_ y
32	29	cxne 11078	. . . . . . . 8 class -e x
33	30, 32, 9	co 6086	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11078	. . . . . . . 8 class -e y
35	29, 34, 9	co 6086	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3786	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6088	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3878	. . . 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 3876	. . 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 3321	. 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 1369	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  17805  xrsex  17806  xrsbas  17807  xrsadd  17808  xrsmul  17809  xrstset  17810  xrsle  17811  xrsds  17831