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 syl6eqr
 |-  ( r = R -> ( lub ` r ) = U )
9 5 imaeq1d
 |-  ( r = R -> ( ( RRHom ` r ) " RR ) = ( ( RRHom ` R ) " RR ) )
10 9 1 syl6eqr
 |-  ( 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 syl6eqr
 |-  ( 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 ) ) ) ) )