Theorem rhmf 20255

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ⟶wf 6536  ‘cfv 6540  (class class class)co 7405  Basecbs 17140   GrpHom cghm 19083   RingHom crh 20240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-plusg 17206  df-0g 17383  df-mhm 18667  df-ghm 19084  df-mgp 19982  df-ur 19999  df-ring 20051  df-rnghom 20243

This theorem is referenced by:  rhmf1o  20261  rhmdvdsr  20279  rhmopp  20280  rnrhmsubrg  20389  imadrhmcl  20405  srngf1o  20454  mulgrhm2  21039  chrrhm  21074  domnchr  21075  znf1o  21098  znidomb  21108  evlslem3  21634  evlslem6  21635  evlslem1  21636  evlseu  21637  mpfconst  21655  mpfproj  21656  mpfsubrg  21657  mpfind  21661  evls1val  21830  evls1sca  21833  evl1val  21839  fveval1fvcl  21843  evl1addd  21851  evl1subd  21852  evl1muld  21853  evl1expd  21855  pf1const  21856  pf1id  21857  pf1subrg  21858  mpfpf1  21861  pf1mpf  21862  pf1ind  21865  ply1remlem  25671  ply1rem  25672  fta1glem1  25674  fta1glem2  25675  fta1g  25676  fta1blem  25677  plypf1  25717  dchrzrhmul  26738  lgsqrlem1  26838  lgsqrlem2  26839  lgsqrlem3  26840  lgseisenlem3  26869  lgseisenlem4  26870  rndrhmcl  32384  rhmdvd  32424  kerunit  32425  fermltlchr  32466  znfermltl  32467  rhmpreimaidl  32525  elrspunidl  32534  rhmimaidl  32538  rhmpreimaprmidl  32558  evls1fn  32628  evls1dm  32629  evls1fvf  32630  evls1expd  32632  evls1fpws  32634  ressply1evl  32635  ply1fermltlchr  32650  elirng  32738  irngss  32739  irngnzply1lem  32742  irngnzply1  32743  mdetlap  32800  rhmpreimacnlem  32852  pl1cn  32923  zrhunitpreima  32946  elzrhunit  32947  qqhval2lem  32949  qqhf  32954  qqhghm  32956  qqhrhm  32957  qqhnm  32958  fldhmf1  40943  imacrhmcl  41086  rimcnv  41089  rhmcomulmpl  41121  rhmmpl  41122  evlscl  41127  evlsexpval  41136  evlsaddval  41137  evlsmulval  41138  evlcl  41141  evladdval  41144  evlmulval  41145  selvcl  41152  idomrootle  41922  elringchom  46865  rhmsscmap2  46870  rhmsscmap  46871  rhmsubcsetclem2  46873  rhmsubcrngclem2  46879  ringcsect  46882  ringcinv  46883  funcringcsetc  46886  funcringcsetcALTV2lem8  46894  funcringcsetcALTV2lem9  46895  elringchomALTV  46900  ringcinvALTV  46907  funcringcsetclem8ALTV  46917  funcringcsetclem9ALTV  46918  zrtermoringc  46921  rhmsubclem4  46940