rhmghm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rhmghm		Structured version Visualization version GIF version

Theorem rhmghm 20458

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 2741	. . . 4 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
2		eqid 2741	. . . 4 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
3	1, 2	isrhm 20453	. . 3 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) ↔ ((𝑅 ∈ Ring ∧ 𝑆 ∈ Ring) ∧ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆)))))
4	3	simprbi 499	. 2 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹 ∈ ((mulGrp‘𝑅) MndHom (mulGrp‘𝑆))))
5	4	simpld 496	1 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2121 ‘cfv 6489 (class class class)co 7360 MndHom cmhm 18744 GrpHom cghm 19182 mulGrpcmgp 20116 Ringcrg 20209 RingHom crh 20444

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-2 12239 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-plusg 17228 df-0g 17399 df-mhm 18746 df-ghm 19183 df-mgp 20117 df-ur 20158 df-ring 20211 df-rhm 20447

This theorem is referenced by: rhmf 20459 rhmf1o 20466 rimgim 20472 rhmco 20476 pwsco2rhm 20478 rhmopp 20485 nrhmzr 20513 rhmimasubrng 20542 resrhm 20577 rhmeql 20579 rhmima 20580 imadrhmcl 20773 srngadd 20827 srng0 20830 rhmpreimaidl 21274 rhmqusnsg 21282 mulgrhm2 21457 zrh0 21492 fermltlchr 21508 chrrhm 21510 zndvds0 21529 zzngim 21531 cygznlem3 21548 zrhpsgnodpm 21571 mplind 22050 evlslem3 22060 evlslem6 22061 evlslem1 22062 evlsgsumadd 22076 evladdval 22083 mpfind 22095 rhmcomulmpl 22104 evlsaddval 22109 selvcllem4 22118 selvvvval 22122 selvadd 22123 selvmul 22124 evls1gsumadd 22314 evl1addd 22331 evl1subd 22332 evls1maplmhm 22367 rhmmpl 22370 rhmply1vr1 22374 rhmply1vsca 22375 ply1rem 26153 plypf1 26199 fxpsubrg 33259 ricnzr1 33373 ricdomn1 33374 znfermltl 33453 rhmquskerlem 33512 rhmqusker 33513 rhmimaidl 33519 mplidomlem 33723 algextdeglem4 33916 zrhf1ker 34169 zrhneg 34174 zrhcntr 34175 qqhghm 34184 qqhrhm 34185 rhmzrhval 42472 fldhmf1 42590 aks6d1c1p2 42609 aks6d1c1p3 42610 aks6d1c5lem1 42636 aks6d1c5lem2 42638 rhmqusspan 42685 aks5lem2 42687 aks5lem3a 42689 ricdrng1 43029 rhmcomulpsr 43047 rhmpsr 43048

W3C validator