Theorem rhmf 20455

Description: A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)

Hypotheses

Ref	Expression
rhmf.b	⊢ 𝐵 = (Base‘𝑅)
rhmf.c	⊢ 𝐶 = (Base‘𝑆)

Assertion

Ref	Expression
rhmf	⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)

Proof of Theorem rhmf

Step	Hyp	Ref	Expression
1		rhmghm 20454	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
2		rhmf.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		rhmf.c	. . 3 ⊢ 𝐶 = (Base‘𝑆)
4	2, 3	ghmf 19186	. 2 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹:𝐵⟶𝐶)
5	1, 4	syl 17	1 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356  Basecbs 17170   GrpHom cghm 19178   RingHom crh 20440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-map 8765  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-plusg 17224  df-0g 17395  df-mhm 18742  df-ghm 19179  df-mgp 20113  df-ur 20154  df-ring 20207  df-rhm 20443

This theorem is referenced by:  rimcnv  20456  rhmf1o  20462  rhmdvdsr  20480  rhmopp  20481  rnrhmsubrg  20577  elringchom  20625  rhmsscmap2  20630  rhmsscmap  20631  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  ringcsect  20642  ringcinv  20643  funcringcsetc  20646  zrtermoringc  20647  rhmsubclem4  20660  imadrhmcl  20769  srngf1o  20820  rhmpreimaidl  21270  mulgrhm2  21453  fermltlchr  21504  chrrhm  21506  domnchr  21507  znf1o  21526  znidomb  21536  evlslem3  22056  evlslem6  22057  evlslem1  22058  evlseu  22059  evlcl  22078  evladdval  22079  evlmulval  22080  mpfconst  22085  mpfproj  22086  mpfsubrg  22087  mpfind  22091  rhmcomulmpl  22100  evlscl  22101  evlsexpval  22104  evlsaddval  22105  evlsmulval  22106  selvcl  22116  ply1fermltlchr  22298  evls1val  22306  evls1sca  22309  evl1val  22315  fveval1fvcl  22319  evl1addd  22327  evl1subd  22328  evl1muld  22329  evl1expd  22331  pf1const  22332  pf1id  22333  pf1subrg  22334  mpfpf1  22337  pf1mpf  22338  pf1ind  22341  evls1expd  22353  evls1fpws  22355  ressply1evl  22356  rhmmpl  22366  rhmply1vr1  22370  rhmply1vsca  22371  ply1remlem  26148  ply1rem  26149  fta1glem1  26151  fta1glem2  26152  fta1g  26153  fta1blem  26154  idomrootle  26156  plypf1  26195  dchrzrhmul  27227  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgseisenlem3  27358  lgseisenlem4  27359  ricdomn1  33370  rndrhmcl  33380  rhmdvd  33407  kerunit  33408  znfermltl  33449  elrspunidl  33511  rhmimaidl  33515  rhmpreimaprmidl  33534  evls1fn  33643  evls1dm  33644  evls1fvf  33645  evl1fvf  33646  mplidomlem  33711  esplyfval0  33748  esplyfval2  33749  esplympl  33751  esplyfval3  33756  vieta  33764  elirng  33870  irngss  33871  irngnzply1lem  33874  irngnzply1  33875  mdetlap  34016  rhmpreimacnlem  34068  pl1cn  34139  zrhunitpreima  34160  elzrhunit  34161  zrhcntr  34163  qqhval2lem  34165  qqhf  34170  qqhghm  34172  qqhrhm  34173  qqhnm  34174  zndvdchrrhm  42458  fldhmf1  42575  aks6d1c1  42601  hashscontpowcl  42605  hashscontpow  42607  aks6d1c4  42609  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem0  42620  aks6d1c5lem3  42622  aks6d1c5lem2  42623  aks6d1c5  42624  aks6d1c6lem1  42655  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem5  42662  aks6d1c7lem1  42665  rhmqusspan  42670  aks5lem2  42672  aks5lem3a  42674  aks5lem5a  42676  imacrhmcl  43004  rhmcomulpsr  43032  rhmpsr  43033  funcringcsetcALTV2lem8  48788  funcringcsetcALTV2lem9  48789  elringchomALTV  48794  ringcinvALTV  48801  funcringcsetclem8ALTV  48811  funcringcsetclem9ALTV  48812