# Metamath Proof Explorer

## Theorem isrhm

Description: A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses isrhm.m ${⊢}{M}={\mathrm{mulGrp}}_{{R}}$
isrhm.n ${⊢}{N}={\mathrm{mulGrp}}_{{S}}$
Assertion isrhm ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({M}\mathrm{MndHom}{N}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 isrhm.m ${⊢}{M}={\mathrm{mulGrp}}_{{R}}$
2 isrhm.n ${⊢}{N}={\mathrm{mulGrp}}_{{S}}$
3 dfrhm2 ${⊢}\mathrm{RingHom}=\left({r}\in \mathrm{Ring},{s}\in \mathrm{Ring}⟼\left({r}\mathrm{GrpHom}{s}\right)\cap \left({\mathrm{mulGrp}}_{{r}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{s}}\right)\right)$
4 3 elmpocl ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)$
5 oveq12 ${⊢}\left({r}={R}\wedge {s}={S}\right)\to {r}\mathrm{GrpHom}{s}={R}\mathrm{GrpHom}{S}$
6 fveq2 ${⊢}{r}={R}\to {\mathrm{mulGrp}}_{{r}}={\mathrm{mulGrp}}_{{R}}$
7 fveq2 ${⊢}{s}={S}\to {\mathrm{mulGrp}}_{{s}}={\mathrm{mulGrp}}_{{S}}$
8 6 7 oveqan12d ${⊢}\left({r}={R}\wedge {s}={S}\right)\to {\mathrm{mulGrp}}_{{r}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{s}}={\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}$
9 5 8 ineq12d ${⊢}\left({r}={R}\wedge {s}={S}\right)\to \left({r}\mathrm{GrpHom}{s}\right)\cap \left({\mathrm{mulGrp}}_{{r}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{s}}\right)=\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)$
10 ovex ${⊢}{R}\mathrm{GrpHom}{S}\in \mathrm{V}$
11 10 inex1 ${⊢}\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\in \mathrm{V}$
12 9 3 11 ovmpoa ${⊢}\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\to {R}\mathrm{RingHom}{S}=\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)$
13 12 eleq2d ${⊢}\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\to \left({F}\in \left({R}\mathrm{RingHom}{S}\right)↔{F}\in \left(\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)\right)$
14 elin ${⊢}{F}\in \left(\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)↔\left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)$
15 1 2 oveq12i ${⊢}{M}\mathrm{MndHom}{N}={\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}$
16 15 eqcomi ${⊢}{\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}={M}\mathrm{MndHom}{N}$
17 16 eleq2i ${⊢}{F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)↔{F}\in \left({M}\mathrm{MndHom}{N}\right)$
18 17 anbi2i ${⊢}\left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)↔\left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({M}\mathrm{MndHom}{N}\right)\right)$
19 14 18 bitri ${⊢}{F}\in \left(\left({R}\mathrm{GrpHom}{S}\right)\cap \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)↔\left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({M}\mathrm{MndHom}{N}\right)\right)$
20 13 19 syl6bb ${⊢}\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\to \left({F}\in \left({R}\mathrm{RingHom}{S}\right)↔\left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({M}\mathrm{MndHom}{N}\right)\right)\right)$
21 4 20 biadanii ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({M}\mathrm{MndHom}{N}\right)\right)\right)$