Metamath Proof Explorer

Theorem xrhval

Description: The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Hypotheses xrhval.b 
|- B = ( ( RRHom ` R ) " RR )
xrhval.l 
|- L = ( glb ` R )
xrhval.u 
|- U = ( lub ` R )
Assertion xrhval 
|- ( R e. V -> ( RR*Hom ` R ) = ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 xrhval.b 
 |-  B = ( ( RRHom ` R ) " RR )
2 xrhval.l 
 |-  L = ( glb ` R )
3 xrhval.u 
 |-  U = ( lub ` R )
4 elex 
 |-  ( R e. V -> R e. _V )
5 fveq2 
 |-  ( r = R -> ( RRHom ` r ) = ( RRHom ` R ) )
6 5 fveq1d 
 |-  ( r = R -> ( ( RRHom ` r ) ` x ) = ( ( RRHom ` R ) ` x ) )
7 fveq2 
 |-  ( r = R -> ( lub ` r ) = ( lub ` R ) )
8 7 3 eqtr4di 
 |-  ( r = R -> ( lub ` r ) = U )
9 5 imaeq1d 
 |-  ( r = R -> ( ( RRHom ` r ) " RR ) = ( ( RRHom ` R ) " RR ) )
10 9 1 eqtr4di 
 |-  ( r = R -> ( ( RRHom ` r ) " RR ) = B )
11 8 10 fveq12d 
 |-  ( r = R -> ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) = ( U ` B ) )
12 fveq2 
 |-  ( r = R -> ( glb ` r ) = ( glb ` R ) )
13 12 2 eqtr4di 
 |-  ( r = R -> ( glb ` r ) = L )
14 13 10 fveq12d 
 |-  ( r = R -> ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) = ( L ` B ) )
15 11 14 ifeq12d 
 |-  ( r = R -> if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) = if ( x = +oo , ( U ` B ) , ( L ` B ) ) )
16 6 15 ifeq12d 
 |-  ( r = R -> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) = if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) )
17 16 mpteq2dv 
 |-  ( r = R -> ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( ( RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( ( RRHom ` r ) " RR ) ) ) ) ) = ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) )
18 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 ) ) ) ) ) )
19 xrex 
 |-  RR* e. _V
20 19 mptex 
 |-  ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) e. _V
21 17 18 20 fvmpt 
 |-  ( R e. _V -> ( RR*Hom ` R ) = ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) )
22 4 21 syl 
 |-  ( R e. V -> ( RR*Hom ` R ) = ( x e. RR* |-> if ( x e. RR , ( ( RRHom ` R ) ` x ) , if ( x = +oo , ( U ` B ) , ( L ` B ) ) ) ) )