Definition df-xrs 13681

Description: The extended real number structure. Unlike df-cnfld 16659, 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 16659. 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 ) , x e >. } 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 13677	. 2 class RR* s
2		cnx 13421	. . . . . 6 class ndx
3		cbs 13424	. . . . . 6 class Base
4	2, 3	cfv 5413	. . . . 5 class ( Base ` ndx )
5		cxr 9075	. . . . 5 class RR*
6	4, 5	cop 3777	. . . 4 class <. ( Base ` ndx ) , RR* >.
7		cplusg 13484	. . . . . 6 class +g
8	2, 7	cfv 5413	. . . . 5 class ( +g ` ndx )
9		cxad 10664	. . . . 5 class + e
10	8, 9	cop 3777	. . . 4 class <. ( +g ` ndx ) , + e >.
11		cmulr 13485	. . . . . 6 class .r
12	2, 11	cfv 5413	. . . . 5 class ( .r ` ndx )
13		cxmu 10665	. . . . 5 class x e
14	12, 13	cop 3777	. . . 4 class <. ( .r ` ndx ) , x e >.
15	6, 10, 14	ctp 3776	. . 3 class { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , + e >. , <. ( .r ` ndx ) , x e >. }
16		cts 13490	. . . . . 6 class TopSet
17	2, 16	cfv 5413	. . . . 5 class (TopSet ` ndx )
18		cle 9077	. . . . . 6 class <_
19		cordt 13676	. . . . . 6 class ordTop
20	18, 19	cfv 5413	. . . . 5 class (ordTop ` <_ )
21	17, 20	cop 3777	. . . 4 class <. (TopSet ` ndx ) , (ordTop ` <_ ) >.
22		cple 13491	. . . . . 6 class le
23	2, 22	cfv 5413	. . . . 5 class ( le ` ndx )
24	23, 18	cop 3777	. . . 4 class <. ( le ` ndx ) , <_ >.
25		cds 13493	. . . . . 6 class dist
26	2, 25	cfv 5413	. . . . 5 class ( dist ` ndx )
27		vx	. . . . . 6 set x
28		vy	. . . . . 6 set y
29	27	cv 1648	. . . . . . . 8 class x
30	28	cv 1648	. . . . . . . 8 class y
31	29, 30, 18	wbr 4172	. . . . . . 7 wff x <_ y
32	29	cxne 10663	. . . . . . . 8 class - e x
33	30, 32, 9	co 6040	. . . . . . 7 class ( y + e - e x )
34	30	cxne 10663	. . . . . . . 8 class - e y
35	29, 34, 9	co 6040	. . . . . . 7 class ( x + e - e y )
36	31, 33, 35	cif 3699	. . . . . 6 class if ( x <_ y , ( y + e - e x ) , ( x + e - e y ) )
37	27, 28, 5, 5, 36	cmpt2 6042	. . . . 5 class ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y + e - e x ) , ( x + e - e y ) ) )
38	26, 37	cop 3777	. . . 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 3776	. . 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 3278	. 2 class ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , + e >. , <. ( .r ` ndx ) , x e >. } 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 1649	1 wff RR* s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , + e >. , <. ( .r ` ndx ) , x e >. } 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  16670  xrsex  16671  xrsbas  16672  xrsadd  16673  xrsmul  16674  xrstset  16675  xrsle  16676  xrsds  16696