# 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}=\mathrm{ℝHom}\left({R}\right)\left[ℝ\right]$
xrhval.l ${⊢}{L}=\mathrm{glb}\left({R}\right)$
xrhval.u ${⊢}{U}=\mathrm{lub}\left({R}\right)$
Assertion xrhval ${⊢}{R}\in {V}\to \mathrm{{ℝ}^{*}Hom}\left({R}\right)=\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 xrhval.b ${⊢}{B}=\mathrm{ℝHom}\left({R}\right)\left[ℝ\right]$
2 xrhval.l ${⊢}{L}=\mathrm{glb}\left({R}\right)$
3 xrhval.u ${⊢}{U}=\mathrm{lub}\left({R}\right)$
4 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
5 fveq2 ${⊢}{r}={R}\to \mathrm{ℝHom}\left({r}\right)=\mathrm{ℝHom}\left({R}\right)$
6 5 fveq1d ${⊢}{r}={R}\to \mathrm{ℝHom}\left({r}\right)\left({x}\right)=\mathrm{ℝHom}\left({R}\right)\left({x}\right)$
7 fveq2 ${⊢}{r}={R}\to \mathrm{lub}\left({r}\right)=\mathrm{lub}\left({R}\right)$
8 7 3 syl6eqr ${⊢}{r}={R}\to \mathrm{lub}\left({r}\right)={U}$
9 5 imaeq1d ${⊢}{r}={R}\to \mathrm{ℝHom}\left({r}\right)\left[ℝ\right]=\mathrm{ℝHom}\left({R}\right)\left[ℝ\right]$
10 9 1 syl6eqr ${⊢}{r}={R}\to \mathrm{ℝHom}\left({r}\right)\left[ℝ\right]={B}$
11 8 10 fveq12d ${⊢}{r}={R}\to \mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)={U}\left({B}\right)$
12 fveq2 ${⊢}{r}={R}\to \mathrm{glb}\left({r}\right)=\mathrm{glb}\left({R}\right)$
13 12 2 syl6eqr ${⊢}{r}={R}\to \mathrm{glb}\left({r}\right)={L}$
14 13 10 fveq12d ${⊢}{r}={R}\to \mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)={L}\left({B}\right)$
15 11 14 ifeq12d ${⊢}{r}={R}\to if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)=if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)$
16 6 15 ifeq12d ${⊢}{r}={R}\to if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)=if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)$
17 16 mpteq2dv ${⊢}{r}={R}\to \left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)=\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)\right)$
18 df-xrh ${⊢}\mathrm{{ℝ}^{*}Hom}=\left({r}\in \mathrm{V}⟼\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)\right)$
19 xrex ${⊢}{ℝ}^{*}\in \mathrm{V}$
20 19 mptex ${⊢}\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)\right)\in \mathrm{V}$
21 17 18 20 fvmpt ${⊢}{R}\in \mathrm{V}\to \mathrm{{ℝ}^{*}Hom}\left({R}\right)=\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)\right)$
22 4 21 syl ${⊢}{R}\in {V}\to \mathrm{{ℝ}^{*}Hom}\left({R}\right)=\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({R}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },{U}\left({B}\right),{L}\left({B}\right)\right)\right)\right)$