Theorem rhmghm 20661

Description: A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)

Assertion

Ref	Expression
rhmghm	⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))

Proof of Theorem rhmghm

Step	Hyp	Ref	Expression
1		eqid 2760	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2		eqid 2760	. . . 4 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
3	1, 2	isrhm 20656	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))))
4	3	simprbi 503	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
5	4	simpld 500	1 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ‘cfv 6528  (class class class)co 7409   MndHom cmhm 18923   GrpHom cghm 19374  mulGrpcmgp 20307  Ringcrg 20406   RingHom crh 20646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233  ax-pre-mulgt0 11234

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7366  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306  df-sub 11500  df-neg 11501  df-nn 12291  df-2 12360  df-sets 17289  df-slot 17307  df-ndx 17319  df-base 17335  df-plusg 17388  df-0g 17559  df-mhm 18925  df-ghm 19375  df-mgp 20308  df-ur 20355  df-ring 20408  df-rhm 20649

This theorem is used by:  rhmf  20662  rhmadd  20665  rhmsub  20666  rhm0  20670  rhmf1o  20674  rimgim  20681  rhmco  20686  rhmkerinj  20687  pwsco2rhm  20689  rhmopp  20706  nrhmzr  20736  rhmimasubrng  20765  resrhm  20800  rhmeql  20802  rhmima  20803  imadrhmcl  21001  srngadd  21055  srng0  21058  rhmpreimaidl  21518  rhmqusnsg  21528  mulgrhm2  21731  zrh0  21766  fermltlchr  21782  chrrhm  21784  zndvds0  21803  zzngim  21805  cygznlem3  21822  zrhpsgnodpm  21845  mplind  22326  evlslem3  22336  evlslem6  22337  evlslem1  22338  evlsgsumadd  22352  evladdval  22359  mpfind  22371  rhmcomulmpl  22380  evlsaddval  22385  selvcllem4  22394  selvvvval  22398  selvadd  22399  selvmul  22400  evls1gsumadd  22589  evl1addd  22606  evl1subd  22607  evls1maplmhm  22642  rhmmpl  22645  rhmply1vr1  22649  rhmply1vsca  22650  ply1rem  26431  plypf1  26478  fxpsubrg  33654  ricnzr1  33768  ricdomn1  33769  znfermltl  33841  rhmquskerlem  33894  rhmqusker  33895  rhmimaidl  33901  mplidomlem  34078  algextdeglem4  34271  zrhf1ker  34524  zrhneg  34529  zrhcntr  34530  qqhghm  34539  qqhrhm  34540  rhmzrhval  42936  fldhmf1  43054  aks6d1c1p2  43073  aks6d1c1p3  43074  aks6d1c5lem1  43100  aks6d1c5lem2  43102  rhmqusspan  43149  aks5lem2  43151  aks5lem3a  43153  ricdrng1  43508  rhmcomulpsr  43526  rhmpsr  43527