Metamath Proof Explorer

Theorem rrhre

Description: The RRHom homomorphism for the real numbers structure is the identity. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion rrhre ( ℝHom ‘ ℝfld ) = ( I ↾ ℝ )

Proof

Step Hyp Ref Expression
1 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
2 rehaus ⊢ ( topGen ‘ ran (,) ) ∈ Haus
3 2 a1i ⊢ ( ⊤ → ( topGen ‘ ran (,) ) ∈ Haus )
4 rerrext ⊢ ℝfld ∈ ℝExt
5 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
6 retopn ⊢ ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
7 5 6 rrhcne ⊢ ( ℝfld ∈ ℝExt → ( ℝHom ‘ ℝfld ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
8 4 7 mp1i ⊢ ( ⊤ → ( ℝHom ‘ ℝfld ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
9 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
10 1 toptopon ⊢ ( ( topGen ‘ ran (,) ) ∈ Top ↔ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
11 9 10 mpbi ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
12 idcn ⊢ ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) → ( I ↾ ℝ ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
13 11 12 ax-mp ⊢ ( I ↾ ℝ ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) )
14 13 a1i ⊢ ( ⊤ → ( I ↾ ℝ ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
15 9 a1i ⊢ ( ⊤ → ( topGen ‘ ran (,) ) ∈ Top )
16 f1oi ⊢ ( I ↾ ℚ ) : ℚ –1-1-onto→ ℚ
17 f1of ⊢ ( ( I ↾ ℚ ) : ℚ –1-1-onto→ ℚ → ( I ↾ ℚ ) : ℚ ⟶ ℚ )
18 16 17 ax-mp ⊢ ( I ↾ ℚ ) : ℚ ⟶ ℚ
19 qssre ⊢ ℚ ⊆ ℝ
20 fss ⊢ ( ( ( I ↾ ℚ ) : ℚ ⟶ ℚ ∧ ℚ ⊆ ℝ ) → ( I ↾ ℚ ) : ℚ ⟶ ℝ )
21 18 19 20 mp2an ⊢ ( I ↾ ℚ ) : ℚ ⟶ ℝ
22 21 a1i ⊢ ( ⊤ → ( I ↾ ℚ ) : ℚ ⟶ ℝ )
23 19 a1i ⊢ ( ⊤ → ℚ ⊆ ℝ )
24 qdensere ⊢ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ
25 24 a1i ⊢ ( ⊤ → ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) = ℝ )
26 9 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( topGen ‘ ran (,) ) ∈ Top )
27 simplr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑎 ∈ ( topGen ‘ ran (,) ) )
28 simpr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑥 ∈ 𝑎 )
29 opnneip ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑎 ∈ ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) )
30 26 27 28 29 syl3anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → 𝑎 ∈ ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) )
31 fvex ⊢ ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ∈ V
32 qex ⊢ ℚ ∈ V
33 elrestr ⊢ ( ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ∈ V ∧ ℚ ∈ V ∧ 𝑎 ∈ ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ) → ( 𝑎 ∩ ℚ ) ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) )
34 31 32 33 mp3an12 ⊢ ( 𝑎 ∈ ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) → ( 𝑎 ∩ ℚ ) ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) )
35 30 34 syl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( 𝑎 ∩ ℚ ) ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) )
36 inss2 ⊢ ( 𝑎 ∩ ℚ ) ⊆ ℚ
37 resiima ⊢ ( ( 𝑎 ∩ ℚ ) ⊆ ℚ → ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) = ( 𝑎 ∩ ℚ ) )
38 36 37 ax-mp ⊢ ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) = ( 𝑎 ∩ ℚ )
39 inss1 ⊢ ( 𝑎 ∩ ℚ ) ⊆ 𝑎
40 38 39 eqsstri ⊢ ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) ⊆ 𝑎
41 40 a1i ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) ⊆ 𝑎 )
42 imaeq2 ⊢ ( 𝑏 = ( 𝑎 ∩ ℚ ) → ( ( I ↾ ℚ ) “ 𝑏 ) = ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) )
43 42 sseq1d ⊢ ( 𝑏 = ( 𝑎 ∩ ℚ ) → ( ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ↔ ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) ⊆ 𝑎 ) )
44 43 rspcev ⊢ ( ( ( 𝑎 ∩ ℚ ) ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∧ ( ( I ↾ ℚ ) “ ( 𝑎 ∩ ℚ ) ) ⊆ 𝑎 ) → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 )
45 35 41 44 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) ∧ 𝑥 ∈ 𝑎 ) → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 )
46 45 ex ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑎 ∈ ( topGen ‘ ran (,) ) ) → ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) )
47 46 ralrimiva ⊢ ( 𝑥 ∈ ℝ → ∀ 𝑎 ∈ ( topGen ‘ ran (,) ) ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) )
48 47 ancli ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ℝ ∧ ∀ 𝑎 ∈ ( topGen ‘ ran (,) ) ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) ) )
49 24 eleq2i ⊢ ( 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ↔ 𝑥 ∈ ℝ )
50 49 biimpri ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) )
51 trnei ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ℚ ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ↔ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∈ ( Fil ‘ ℚ ) ) )
52 11 19 51 mp3an12 ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ( cls ‘ ( topGen ‘ ran (,) ) ) ‘ ℚ ) ↔ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∈ ( Fil ‘ ℚ ) ) )
53 50 52 mpbid ⊢ ( 𝑥 ∈ ℝ → ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∈ ( Fil ‘ ℚ ) )
54 isflf ⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∈ ( Fil ‘ ℚ ) ∧ ( I ↾ ℚ ) : ℚ ⟶ ℝ ) → ( 𝑥 ∈ ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ∀ 𝑎 ∈ ( topGen ‘ ran (,) ) ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) ) ) )
55 11 21 54 mp3an13 ⊢ ( ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ∈ ( Fil ‘ ℚ ) → ( 𝑥 ∈ ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ∀ 𝑎 ∈ ( topGen ‘ ran (,) ) ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) ) ) )
56 53 55 syl ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ∀ 𝑎 ∈ ( topGen ‘ ran (,) ) ( 𝑥 ∈ 𝑎 → ∃ 𝑏 ∈ ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ( ( I ↾ ℚ ) “ 𝑏 ) ⊆ 𝑎 ) ) ) )
57 48 56 mpbird ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) )
58 57 ne0d ⊢ ( 𝑥 ∈ ℝ → ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) ≠ ∅ )
59 58 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( ( ( topGen ‘ ran (,) ) fLimf ( ( ( nei ‘ ( topGen ‘ ran (,) ) ) ‘ { 𝑥 } ) ↾t ℚ ) ) ‘ ( I ↾ ℚ ) ) ≠ ∅ )
60 recusp ⊢ ℝfld ∈ CUnifSp
61 cuspusp ⊢ ( ℝfld ∈ CUnifSp → ℝfld ∈ UnifSp )
62 60 61 ax-mp ⊢ ℝfld ∈ UnifSp
63 6 uspreg ⊢ ( ( ℝfld ∈ UnifSp ∧ ( topGen ‘ ran (,) ) ∈ Haus ) → ( topGen ‘ ran (,) ) ∈ Reg )
64 62 2 63 mp2an ⊢ ( topGen ‘ ran (,) ) ∈ Reg
65 64 a1i ⊢ ( ⊤ → ( topGen ‘ ran (,) ) ∈ Reg )
66 resabs1 ⊢ ( ℚ ⊆ ℝ → ( ( I ↾ ℝ ) ↾ ℚ ) = ( I ↾ ℚ ) )
67 19 66 ax-mp ⊢ ( ( I ↾ ℝ ) ↾ ℚ ) = ( I ↾ ℚ )
68 1 cnrest ⊢ ( ( ( I ↾ ℝ ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ∧ ℚ ⊆ ℝ ) → ( ( I ↾ ℝ ) ↾ ℚ ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( topGen ‘ ran (,) ) ) )
69 13 19 68 mp2an ⊢ ( ( I ↾ ℝ ) ↾ ℚ ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( topGen ‘ ran (,) ) )
70 67 69 eqeltrri ⊢ ( I ↾ ℚ ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( topGen ‘ ran (,) ) )
71 70 a1i ⊢ ( ⊤ → ( I ↾ ℚ ) ∈ ( ( ( topGen ‘ ran (,) ) ↾t ℚ ) Cn ( topGen ‘ ran (,) ) ) )
72 1 1 15 3 22 23 25 59 65 71 cnextfres1 ⊢ ( ⊤ → ( ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( I ↾ ℚ ) ) ↾ ℚ ) = ( I ↾ ℚ ) )
73 72 mptru ⊢ ( ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( I ↾ ℚ ) ) ↾ ℚ ) = ( I ↾ ℚ )
74 recms ⊢ ℝfld ∈ CMetSp
75 74 elexi ⊢ ℝfld ∈ V
76 5 6 rrhval ⊢ ( ℝfld ∈ V → ( ℝHom ‘ ℝfld ) = ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( ℚHom ‘ ℝfld ) ) )
77 75 76 ax-mp ⊢ ( ℝHom ‘ ℝfld ) = ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( ℚHom ‘ ℝfld ) )
78 qqhre ⊢ ( ℚHom ‘ ℝfld ) = ( I ↾ ℚ )
79 78 fveq2i ⊢ ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( ℚHom ‘ ℝfld ) ) = ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( I ↾ ℚ ) )
80 77 79 eqtri ⊢ ( ℝHom ‘ ℝfld ) = ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( I ↾ ℚ ) )
81 80 reseq1i ⊢ ( ( ℝHom ‘ ℝfld ) ↾ ℚ ) = ( ( ( ( topGen ‘ ran (,) ) CnExt ( topGen ‘ ran (,) ) ) ‘ ( I ↾ ℚ ) ) ↾ ℚ )
82 73 81 67 3eqtr4i ⊢ ( ( ℝHom ‘ ℝfld ) ↾ ℚ ) = ( ( I ↾ ℝ ) ↾ ℚ )
83 82 a1i ⊢ ( ⊤ → ( ( ℝHom ‘ ℝfld ) ↾ ℚ ) = ( ( I ↾ ℝ ) ↾ ℚ ) )
84 1 3 8 14 83 23 25 hauseqcn ⊢ ( ⊤ → ( ℝHom ‘ ℝfld ) = ( I ↾ ℝ ) )
85 84 mptru ⊢ ( ℝHom ‘ ℝfld ) = ( I ↾ ℝ )