Definition df-xrs

Description: The extended real number structure. Unlike df-cnfld , 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 . 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 CCfld when restricted to RR . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	df-xrs	⊢ ℝ*𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxrs	⊢ ℝ*𝑠
1		cbs	⊢ Base
2		cnx	⊢ ndx
3	2 1	cfv	⊢ ( Base ‘ ndx )
4		cxr	⊢ ℝ*
5	3 4	cop	⊢ ⟨ ( Base ‘ ndx ) , ℝ* ⟩
6		cplusg	⊢ +g
7	2 6	cfv	⊢ ( +g ‘ ndx )
8		cxad	⊢ +𝑒
9	7 8	cop	⊢ ⟨ ( +g ‘ ndx ) , +𝑒 ⟩
10		cmulr	⊢ .r
11	2 10	cfv	⊢ ( .r ‘ ndx )
12		cxmu	⊢ ·e
13	11 12	cop	⊢ ⟨ ( .r ‘ ndx ) , ·e ⟩
14	5 9 13	ctp	⊢ { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ }
15		cts	⊢ TopSet
16	2 15	cfv	⊢ ( TopSet ‘ ndx )
17		cordt	⊢ ordTop
18		cle	⊢ ≤
19	18 17	cfv	⊢ ( ordTop ‘ ≤ )
20	16 19	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩
21		cple	⊢ le
22	2 21	cfv	⊢ ( le ‘ ndx )
23	22 18	cop	⊢ ⟨ ( le ‘ ndx ) , ≤ ⟩
24		cds	⊢ dist
25	2 24	cfv	⊢ ( dist ‘ ndx )
26		vx	⊢ 𝑥
27		vy	⊢ 𝑦
28	26	cv	⊢ 𝑥
29	27	cv	⊢ 𝑦
30	28 29 18	wbr	⊢ 𝑥 ≤ 𝑦
31	28	cxne	⊢ -𝑒 𝑥
32	29 31 8	co	⊢ ( 𝑦 +𝑒 -𝑒 𝑥 )
33	29	cxne	⊢ -𝑒 𝑦
34	28 33 8	co	⊢ ( 𝑥 +𝑒 -𝑒 𝑦 )
35	30 32 34	cif	⊢ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) )
36	26 27 4 4 35	cmpo	⊢ ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) )
37	25 36	cop	⊢ ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩
38	20 23 37	ctp	⊢ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ }
39	14 38	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } )
40	0 39	wceq	⊢ ℝ*𝑠 = ( { ⟨ ( Base ‘ ndx ) , ℝ* ⟩ , ⟨ ( +g ‘ ndx ) , +𝑒 ⟩ , ⟨ ( .r ‘ ndx ) , ·e ⟩ } ∪ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ if ( 𝑥 ≤ 𝑦 , ( 𝑦 +𝑒 -𝑒 𝑥 ) , ( 𝑥 +𝑒 -𝑒 𝑦 ) ) ) ⟩ } )