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 = ℝHom ⁡ R ℝ
xrhval.l ⊢ L = glb ⁡ R
xrhval.u ⊢ U = lub ⁡ R
Assertion xrhval ⊢ R ∈ V → ℝ *Hom ⁡ R = x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B

Proof

Step Hyp Ref Expression
1 xrhval.b ⊢ B = ℝHom ⁡ R ℝ
2 xrhval.l ⊢ L = glb ⁡ R
3 xrhval.u ⊢ U = lub ⁡ R
4 elex ⊢ R ∈ V → R ∈ V
5 fveq2 ⊢ r = R → ℝHom ⁡ r = ℝHom ⁡ R
6 5 fveq1d ⊢ r = R → ℝHom ⁡ r ⁡ x = ℝHom ⁡ R ⁡ x
7 fveq2 ⊢ r = R → lub ⁡ r = lub ⁡ R
8 7 3 eqtr4di ⊢ r = R → lub ⁡ r = U
9 5 imaeq1d ⊢ r = R → ℝHom ⁡ r ℝ = ℝHom ⁡ R ℝ
10 9 1 eqtr4di ⊢ r = R → ℝHom ⁡ r ℝ = B
11 8 10 fveq12d ⊢ r = R → lub ⁡ r ⁡ ℝHom ⁡ r ℝ = 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 ⁡ ℝHom ⁡ r ℝ = L ⁡ B
15 11 14 ifeq12d ⊢ r = R → if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ = if x = +∞ U ⁡ B L ⁡ B
16 6 15 ifeq12d ⊢ r = R → if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ = if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B
17 16 mpteq2dv ⊢ r = R → x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ = x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B
18 df-xrh ⊢ ℝ *Hom = r ∈ V ⟼ x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ
19 xrex ⊢ ℝ * ∈ V
20 19 mptex ⊢ x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B ∈ V
21 17 18 20 fvmpt ⊢ R ∈ V → ℝ *Hom ⁡ R = x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B
22 4 21 syl ⊢ R ∈ V → ℝ *Hom ⁡ R = x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ R ⁡ x if x = +∞ U ⁡ B L ⁡ B