Theorem rhmf 20379

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 20378	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
2		rhmf.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
3		rhmf.c	. . 3 ⊢ 𝐶 = (Base‘𝑆)
4	2, 3	ghmf 19137	. 2 ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹:𝐵⟶𝐶)
5	1, 4	syl 17	1 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐵⟶𝐶)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ⟶wf 6530  ‘cfv 6534  (class class class)co 7402  Basecbs 17145   GrpHom cghm 19130   RingHom crh 20363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-2 12273  df-sets 17098  df-slot 17116  df-ndx 17128  df-base 17146  df-plusg 17211  df-0g 17388  df-mhm 18705  df-ghm 19131  df-mgp 20032  df-ur 20079  df-ring 20132  df-rhm 20366

This theorem is referenced by:  rhmf1o  20385  rhmdvdsr  20402  rhmopp  20403  rnrhmsubrg  20499  elringchom  20541  rhmsscmap2  20546  rhmsscmap  20547  rhmsubcsetclem2  20549  rhmsubcrngclem2  20555  ringcsect  20558  ringcinv  20559  funcringcsetc  20562  zrtermoringc  20563  rhmsubclem4  20576  imadrhmcl  20640  srngf1o  20689  mulgrhm2  21335  fermltlchr  21390  chrrhm  21392  domnchr  21393  znf1o  21416  znidomb  21426  evlslem3  21955  evlslem6  21956  evlslem1  21957  evlseu  21958  mpfconst  21976  mpfproj  21977  mpfsubrg  21978  mpfind  21982  ply1fermltlchr  22155  evls1val  22163  evls1sca  22166  evl1val  22172  fveval1fvcl  22176  evl1addd  22184  evl1subd  22185  evl1muld  22186  evl1expd  22188  pf1const  22189  pf1id  22190  pf1subrg  22191  mpfpf1  22194  pf1mpf  22195  pf1ind  22198  ply1remlem  26022  ply1rem  26023  fta1glem1  26025  fta1glem2  26026  fta1g  26027  fta1blem  26028  plypf1  26068  dchrzrhmul  27098  lgsqrlem1  27198  lgsqrlem2  27199  lgsqrlem3  27200  lgseisenlem3  27229  lgseisenlem4  27230  rndrhmcl  32865  rhmdvd  32905  kerunit  32906  znfermltl  32951  rhmpreimaidl  33009  elrspunidl  33018  rhmimaidl  33022  rhmpreimaprmidl  33042  evls1fn  33110  evls1dm  33111  evls1fvf  33112  evls1expd  33114  evls1fpws  33116  ressply1evl  33117  elirng  33233  irngss  33234  irngnzply1lem  33237  irngnzply1  33238  mdetlap  33304  rhmpreimacnlem  33356  pl1cn  33427  zrhunitpreima  33450  elzrhunit  33451  qqhval2lem  33453  qqhf  33458  qqhghm  33460  qqhrhm  33461  qqhnm  33462  fldhmf1  41452  imacrhmcl  41584  rimcnv  41587  rhmcomulmpl  41617  rhmmpl  41618  evlscl  41623  evlsexpval  41632  evlsaddval  41633  evlsmulval  41634  evlcl  41637  evladdval  41640  evlmulval  41641  selvcl  41648  idomrootle  42451  funcringcsetcALTV2lem8  47185  funcringcsetcALTV2lem9  47186  elringchomALTV  47191  ringcinvALTV  47198  funcringcsetclem8ALTV  47208  funcringcsetclem9ALTV  47209