# 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 ) ) ) ) )`