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	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( lub ‘ 𝑟 ) = 𝑈 )
9	5	imaeq1d	⊢ ( 𝑟 = 𝑅 → ( ( ℝHom ‘ 𝑟 ) “ ℝ ) = ( ( ℝHom ‘ 𝑅 ) “ ℝ ) )
10	9 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( ( ℝHom ‘ 𝑟 ) “ ℝ ) = 𝐵 )
11	8 10	fveq12d	⊢ ( 𝑟 = 𝑅 → ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) = ( 𝑈 ‘ 𝐵 ) )
12		fveq2	⊢ ( 𝑟 = 𝑅 → ( glb ‘ 𝑟 ) = ( glb ‘ 𝑅 ) )
13	12 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 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 ( 𝑥 = +∞ , ( 𝑈 ‘ 𝐵 ) , ( 𝐿 ‘ 𝐵 ) ) ) ) )

Metamath Proof Explorer

Theorem xrhval

Proof