Metamath Proof Explorer


Definition df-rrh

Description: Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017) (Revised by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Assertion df-rrh ℝHom = ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crrh ℝHom
1 vr 𝑟
2 cvv V
3 ctg topGen
4 cioo (,)
5 4 crn ran (,)
6 5 3 cfv ( topGen ‘ ran (,) )
7 ccnext CnExt
8 ctopn TopOpen
9 1 cv 𝑟
10 9 8 cfv ( TopOpen ‘ 𝑟 )
11 6 10 7 co ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) )
12 cqqh ℚHom
13 9 12 cfv ( ℚHom ‘ 𝑟 )
14 13 11 cfv ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) )
15 1 2 14 cmpt ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )
16 0 15 wceq ℝHom = ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )