Metamath Proof Explorer

Definition df-xrh

Description: Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Assertion df-xrh 
|- RR*Hom = ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxrh 
 |-  RR*Hom
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cxr 
 |-  RR*
5 3 cv 
 |-  x
6 cr 
 |-  RR
7 5 6 wcel 
 |-  x e. RR
8 crrh 
 |-  RRHom
9 1 cv 
 |-  r
10 9 8 cfv 
 |-  ( RRHom ` r )
11 5 10 cfv 
 |-  ( ( RRHom ` r ) ` x )
12 cpnf 
 |-  +oo
13 5 12 wceq 
 |-  x = +oo
14 club 
 |-  lub
15 9 14 cfv 
 |-  ( lub ` r )
16 10 6 cima 
 |-  ( ( RRHom ` r ) " RR )
17 16 15 cfv 
 |-  ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) )
18 cglb 
 |-  glb
19 9 18 cfv 
 |-  ( glb ` r )
20 16 19 cfv 
 |-  ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) )
21 13 17 20 cif 
 |-  if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) )
22 7 11 21 cif 
 |-  if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) )
23 3 4 22 cmpt 
 |-  ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) )
24 1 2 23 cmpt 
 |-  ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) ) )
25 0 24 wceq 
 |-  RR*Hom = ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) ) )