Definition df-xrs 14423

Description: The extended real number structure. Unlike df-cnfld 17663, 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 17663. 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 14421	. 2 class RR*s
2		cnx 14154	. . . . . 6 class ndx
3		cbs 14157	. . . . . 6 class Base
4	2, 3	cfv 5406	. . . . 5 class ( Base ` ndx )
5		cxr 9405	. . . . 5 class RR*
6	4, 5	cop 3871	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 14221	. . . . . 6 class +g
8	2, 7	cfv 5406	. . . . 5 class ( +g ` ndx )
9		cxad 11075	. . . . 5 class +e
10	8, 9	cop 3871	. . . 4 class <. ( +g ` ndx ) , +e >.
11		cmulr 14222	. . . . . 6 class .r
12	2, 11	cfv 5406	. . . . 5 class ( .r ` ndx )
13		cxmu 11076	. . . . 5 class xe
14	12, 13	cop 3871	. . . 4 class <. ( .r ` ndx ) , xe >.
15	6, 10, 14	ctp 3869	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , xe >. }
16		cts 14227	. . . . . 6 class TopSet
17	2, 16	cfv 5406	. . . . 5 class (TopSet ` ndx )
18		cle 9407	. . . . . 6 class <_
19		cordt 14420	. . . . . 6 class ordTop
20	18, 19	cfv 5406	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3871	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 14228	. . . . . 6 class le
23	2, 22	cfv 5406	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3871	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 14230	. . . . . 6 class dist
26	2, 25	cfv 5406	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 setvar x
28		vy	. . . . . 6 setvar y
29	27	cv 1361	. . . . . . . 8 class x
30	28	cv 1361	. . . . . . . 8 class y
31	29, 30, 18	wbr 4280	. . . . . . 7 wff x <_ y
32	29	cxne 11074	. . . . . . . 8 class -e x
33	30, 32, 9	co 6080	. . . . . . 7 class ( y +e -e x )
34	30	cxne 11074	. . . . . . . 8 class -e y
35	29, 34, 9	co 6080	. . . . . . 7 class ( x +e -e y )
36	31, 33, 35	cif 3779	. . . . . 6 class if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) )
37	27, 28, 5, 5, 36	cmpt2 6082	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) )
38	26, 37	cop 3871	. . . 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 3869	. . 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 3314	. 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 1362	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  17674  xrsex  17675  xrsbas  17676  xrsadd  17677  xrsmul  17678  xrstset  17679  xrsle  17680  xrsds  17700