![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrhqima | Structured version Visualization version GIF version |
Description: The ℝHom homomorphism leaves rational numbers unchanged. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
Ref | Expression |
---|---|
rrhqima | ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2826 | . . . . 5 ⊢ (topGen‘ran (,)) = (topGen‘ran (,)) | |
2 | eqid 2826 | . . . . 5 ⊢ (TopOpen‘𝑅) = (TopOpen‘𝑅) | |
3 | 1, 2 | rrhval 30586 | . . . 4 ⊢ (𝑅 ∈ ℝExt → (ℝHom‘𝑅) = (((topGen‘ran (,))CnExt(TopOpen‘𝑅))‘(ℚHom‘𝑅))) |
4 | 3 | fveq1d 6436 | . . 3 ⊢ (𝑅 ∈ ℝExt → ((ℝHom‘𝑅)‘𝑄) = ((((topGen‘ran (,))CnExt(TopOpen‘𝑅))‘(ℚHom‘𝑅))‘𝑄)) |
5 | 4 | adantr 474 | . 2 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((((topGen‘ran (,))CnExt(TopOpen‘𝑅))‘(ℚHom‘𝑅))‘𝑄)) |
6 | uniretop 22937 | . . 3 ⊢ ℝ = ∪ (topGen‘ran (,)) | |
7 | eqid 2826 | . . 3 ⊢ ∪ (TopOpen‘𝑅) = ∪ (TopOpen‘𝑅) | |
8 | retop 22936 | . . . 4 ⊢ (topGen‘ran (,)) ∈ Top | |
9 | 8 | a1i 11 | . . 3 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → (topGen‘ran (,)) ∈ Top) |
10 | 2 | rrexthaus 30597 | . . . 4 ⊢ (𝑅 ∈ ℝExt → (TopOpen‘𝑅) ∈ Haus) |
11 | 10 | adantr 474 | . . 3 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → (TopOpen‘𝑅) ∈ Haus) |
12 | qssre 12082 | . . . 4 ⊢ ℚ ⊆ ℝ | |
13 | 12 | a1i 11 | . . 3 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ℚ ⊆ ℝ) |
14 | rrextnrg 30591 | . . . . . . 7 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing) | |
15 | rrextdrg 30592 | . . . . . . 7 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing) | |
16 | 14, 15 | elind 4026 | . . . . . 6 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ (NrmRing ∩ DivRing)) |
17 | eqid 2826 | . . . . . . 7 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅) | |
18 | 17 | rrextnlm 30593 | . . . . . 6 ⊢ (𝑅 ∈ ℝExt → (ℤMod‘𝑅) ∈ NrmMod) |
19 | rrextchr 30594 | . . . . . 6 ⊢ (𝑅 ∈ ℝExt → (chr‘𝑅) = 0) | |
20 | eqid 2826 | . . . . . . 7 ⊢ (ℂfld ↾s ℚ) = (ℂfld ↾s ℚ) | |
21 | qqtopn 30601 | . . . . . . 7 ⊢ ((TopOpen‘ℝfld) ↾t ℚ) = (TopOpen‘(ℂfld ↾s ℚ)) | |
22 | 20, 21, 17, 2 | qqhcn 30581 | . . . . . 6 ⊢ ((𝑅 ∈ (NrmRing ∩ DivRing) ∧ (ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) → (ℚHom‘𝑅) ∈ (((TopOpen‘ℝfld) ↾t ℚ) Cn (TopOpen‘𝑅))) |
23 | 16, 18, 19, 22 | syl3anc 1496 | . . . . 5 ⊢ (𝑅 ∈ ℝExt → (ℚHom‘𝑅) ∈ (((TopOpen‘ℝfld) ↾t ℚ) Cn (TopOpen‘𝑅))) |
24 | retopn 23548 | . . . . . . . 8 ⊢ (topGen‘ran (,)) = (TopOpen‘ℝfld) | |
25 | 24 | eqcomi 2835 | . . . . . . 7 ⊢ (TopOpen‘ℝfld) = (topGen‘ran (,)) |
26 | 25 | oveq1i 6916 | . . . . . 6 ⊢ ((TopOpen‘ℝfld) ↾t ℚ) = ((topGen‘ran (,)) ↾t ℚ) |
27 | 26 | oveq1i 6916 | . . . . 5 ⊢ (((TopOpen‘ℝfld) ↾t ℚ) Cn (TopOpen‘𝑅)) = (((topGen‘ran (,)) ↾t ℚ) Cn (TopOpen‘𝑅)) |
28 | 23, 27 | syl6eleq 2917 | . . . 4 ⊢ (𝑅 ∈ ℝExt → (ℚHom‘𝑅) ∈ (((topGen‘ran (,)) ↾t ℚ) Cn (TopOpen‘𝑅))) |
29 | 28 | adantr 474 | . . 3 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → (ℚHom‘𝑅) ∈ (((topGen‘ran (,)) ↾t ℚ) Cn (TopOpen‘𝑅))) |
30 | simpr 479 | . . 3 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → 𝑄 ∈ ℚ) | |
31 | 6, 7, 9, 11, 13, 29, 30 | cnextfres 22244 | . 2 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((((topGen‘ran (,))CnExt(TopOpen‘𝑅))‘(ℚHom‘𝑅))‘𝑄) = ((ℚHom‘𝑅)‘𝑄)) |
32 | 5, 31 | eqtrd 2862 | 1 ⊢ ((𝑅 ∈ ℝExt ∧ 𝑄 ∈ ℚ) → ((ℝHom‘𝑅)‘𝑄) = ((ℚHom‘𝑅)‘𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ∩ cin 3798 ⊆ wss 3799 ∪ cuni 4659 ran crn 5344 ‘cfv 6124 (class class class)co 6906 ℝcr 10252 0cc0 10253 ℚcq 12072 (,)cioo 12464 ↾s cress 16224 ↾t crest 16435 TopOpenctopn 16436 topGenctg 16452 DivRingcdr 19104 ℂfldccnfld 20107 ℤModczlm 20210 chrcchr 20211 ℝfldcrefld 20312 Topctop 21069 Cn ccn 21400 Hauscha 21484 CnExtccnext 22234 NrmRingcnrg 22755 NrmModcnlm 22756 ℚHomcqqh 30562 ℝHomcrrh 30583 ℝExt crrext 30584 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-inf2 8816 ax-cnex 10309 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-addrcl 10314 ax-mulcl 10315 ax-mulrcl 10316 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-i2m1 10321 ax-1ne0 10322 ax-1rid 10323 ax-rnegex 10324 ax-rrecex 10325 ax-cnre 10326 ax-pre-lttri 10327 ax-pre-lttrn 10328 ax-pre-ltadd 10329 ax-pre-mulgt0 10330 ax-pre-sup 10331 ax-addf 10332 ax-mulf 10333 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-reu 3125 df-rmo 3126 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-int 4699 df-iun 4743 df-iin 4744 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-se 5303 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-pred 5921 df-ord 5967 df-on 5968 df-lim 5969 df-suc 5970 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-isom 6133 df-riota 6867 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-of 7158 df-om 7328 df-1st 7429 df-2nd 7430 df-supp 7561 df-tpos 7618 df-wrecs 7673 df-recs 7735 df-rdg 7773 df-1o 7827 df-2o 7828 df-oadd 7831 df-er 8010 df-map 8125 df-pm 8126 df-ixp 8177 df-en 8224 df-dom 8225 df-sdom 8226 df-fin 8227 df-fsupp 8546 df-fi 8587 df-sup 8618 df-inf 8619 df-oi 8685 df-card 9079 df-cda 9306 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-sub 10588 df-neg 10589 df-div 11011 df-nn 11352 df-2 11415 df-3 11416 df-4 11417 df-5 11418 df-6 11419 df-7 11420 df-8 11421 df-9 11422 df-n0 11620 df-z 11706 df-dec 11823 df-uz 11970 df-q 12073 df-rp 12114 df-xneg 12233 df-xadd 12234 df-xmul 12235 df-ioo 12468 df-ico 12470 df-icc 12471 df-fz 12621 df-fzo 12762 df-fl 12889 df-mod 12965 df-seq 13097 df-exp 13156 df-hash 13412 df-cj 14217 df-re 14218 df-im 14219 df-sqrt 14353 df-abs 14354 df-dvds 15359 df-gcd 15591 df-numer 15815 df-denom 15816 df-gz 16006 df-struct 16225 df-ndx 16226 df-slot 16227 df-base 16229 df-sets 16230 df-ress 16231 df-plusg 16319 df-mulr 16320 df-starv 16321 df-sca 16322 df-vsca 16323 df-ip 16324 df-tset 16325 df-ple 16326 df-ds 16328 df-unif 16329 df-hom 16330 df-cco 16331 df-rest 16437 df-topn 16438 df-0g 16456 df-gsum 16457 df-topgen 16458 df-pt 16459 df-prds 16462 df-xrs 16516 df-qtop 16521 df-imas 16522 df-xps 16524 df-mre 16600 df-mrc 16601 df-acs 16603 df-plusf 17595 df-mgm 17596 df-sgrp 17638 df-mnd 17649 df-mhm 17689 df-submnd 17690 df-grp 17780 df-minusg 17781 df-sbg 17782 df-mulg 17896 df-subg 17943 df-ghm 18010 df-cntz 18101 df-od 18300 df-cmn 18549 df-abl 18550 df-mgp 18845 df-ur 18857 df-ring 18904 df-cring 18905 df-oppr 18978 df-dvdsr 18996 df-unit 18997 df-invr 19027 df-dvr 19038 df-rnghom 19072 df-drng 19106 df-subrg 19135 df-abv 19174 df-lmod 19222 df-scaf 19223 df-sra 19534 df-rgmod 19535 df-nzr 19620 df-psmet 20099 df-xmet 20100 df-met 20101 df-bl 20102 df-mopn 20103 df-fbas 20104 df-fg 20105 df-cnfld 20108 df-zring 20180 df-zrh 20213 df-zlm 20214 df-chr 20215 df-refld 20313 df-top 21070 df-topon 21087 df-topsp 21109 df-bases 21122 df-cld 21195 df-ntr 21196 df-cls 21197 df-nei 21274 df-cn 21403 df-cnp 21404 df-haus 21491 df-tx 21737 df-hmeo 21930 df-fil 22021 df-fm 22113 df-flim 22114 df-flf 22115 df-cnext 22235 df-tmd 22247 df-tgp 22248 df-trg 22334 df-xms 22496 df-ms 22497 df-tms 22498 df-nm 22758 df-ngp 22759 df-nrg 22761 df-nlm 22762 df-qqh 30563 df-rrh 30585 df-rrext 30589 |
This theorem is referenced by: rrh0 30605 |
Copyright terms: Public domain | W3C validator |