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 𝐵 = ( ( ℝHom ‘ 𝑅 ) “ ℝ )
xrhval.l 𝐿 = ( glb ‘ 𝑅 )
xrhval.u 𝑈 = ( lub ‘ 𝑅 )
Assertion xrhval ( 𝑅𝑉 → ( ℝ*Hom ‘ 𝑅 ) = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 xrhval.b 𝐵 = ( ( ℝHom ‘ 𝑅 ) “ ℝ )
2 xrhval.l 𝐿 = ( glb ‘ 𝑅 )
3 xrhval.u 𝑈 = ( lub ‘ 𝑅 )
4 elex ( 𝑅𝑉𝑅 ∈ V )
5 fveq2 ( 𝑟 = 𝑅 → ( ℝHom ‘ 𝑟 ) = ( ℝHom ‘ 𝑅 ) )
6 5 fveq1d ( 𝑟 = 𝑅 → ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) = ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) )
7 fveq2 ( 𝑟 = 𝑅 → ( lub ‘ 𝑟 ) = ( lub ‘ 𝑅 ) )
8 7 3 syl6eqr ( 𝑟 = 𝑅 → ( lub ‘ 𝑟 ) = 𝑈 )
9 5 imaeq1d ( 𝑟 = 𝑅 → ( ( ℝHom ‘ 𝑟 ) “ ℝ ) = ( ( ℝHom ‘ 𝑅 ) “ ℝ ) )
10 9 1 syl6eqr ( 𝑟 = 𝑅 → ( ( ℝHom ‘ 𝑟 ) “ ℝ ) = 𝐵 )
11 8 10 fveq12d ( 𝑟 = 𝑅 → ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) = ( 𝑈𝐵 ) )
12 fveq2 ( 𝑟 = 𝑅 → ( glb ‘ 𝑟 ) = ( glb ‘ 𝑅 ) )
13 12 2 syl6eqr ( 𝑟 = 𝑅 → ( glb ‘ 𝑟 ) = 𝐿 )
14 13 10 fveq12d ( 𝑟 = 𝑅 → ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) = ( 𝐿𝐵 ) )
15 11 14 ifeq12d ( 𝑟 = 𝑅 → if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) = if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) )
16 6 15 ifeq12d ( 𝑟 = 𝑅 → if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) = if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) )
17 16 mpteq2dv ( 𝑟 = 𝑅 → ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) ) = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) ) )
18 df-xrh *Hom = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) ) )
19 xrex * ∈ V
20 19 mptex ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) ) ∈ V
21 17 18 20 fvmpt ( 𝑅 ∈ V → ( ℝ*Hom ‘ 𝑅 ) = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) ) )
22 4 21 syl ( 𝑅𝑉 → ( ℝ*Hom ‘ 𝑅 ) = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑅 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( 𝑈𝐵 ) , ( 𝐿𝐵 ) ) ) ) )