# Metamath Proof Explorer

## Theorem resrhm

Description: Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypothesis resrhm.u ${⊢}{U}={S}{↾}_{𝑠}{X}$
Assertion resrhm ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left({U}\mathrm{RingHom}{T}\right)$

### Proof

Step Hyp Ref Expression
1 resrhm.u ${⊢}{U}={S}{↾}_{𝑠}{X}$
2 rhmrcl2 ${⊢}{F}\in \left({S}\mathrm{RingHom}{T}\right)\to {T}\in \mathrm{Ring}$
3 1 subrgring ${⊢}{X}\in \mathrm{SubRing}\left({S}\right)\to {U}\in \mathrm{Ring}$
4 2 3 anim12ci ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({U}\in \mathrm{Ring}\wedge {T}\in \mathrm{Ring}\right)$
5 rhmghm ${⊢}{F}\in \left({S}\mathrm{RingHom}{T}\right)\to {F}\in \left({S}\mathrm{GrpHom}{T}\right)$
6 subrgsubg ${⊢}{X}\in \mathrm{SubRing}\left({S}\right)\to {X}\in \mathrm{SubGrp}\left({S}\right)$
7 1 resghm ${⊢}\left({F}\in \left({S}\mathrm{GrpHom}{T}\right)\wedge {X}\in \mathrm{SubGrp}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left({U}\mathrm{GrpHom}{T}\right)$
8 5 6 7 syl2an ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left({U}\mathrm{GrpHom}{T}\right)$
9 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}={\mathrm{mulGrp}}_{{S}}$
10 eqid ${⊢}{\mathrm{mulGrp}}_{{T}}={\mathrm{mulGrp}}_{{T}}$
11 9 10 rhmmhm ${⊢}{F}\in \left({S}\mathrm{RingHom}{T}\right)\to {F}\in \left({\mathrm{mulGrp}}_{{S}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)$
12 9 subrgsubm ${⊢}{X}\in \mathrm{SubRing}\left({S}\right)\to {X}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{S}}\right)$
13 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}={\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}$
14 13 resmhm ${⊢}\left({F}\in \left({\mathrm{mulGrp}}_{{S}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)\wedge {X}\in \mathrm{SubMnd}\left({\mathrm{mulGrp}}_{{S}}\right)\right)\to {{F}↾}_{{X}}\in \left(\left({\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)$
15 11 12 14 syl2an ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left(\left({\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)$
16 rhmrcl1 ${⊢}{F}\in \left({S}\mathrm{RingHom}{T}\right)\to {S}\in \mathrm{Ring}$
17 1 9 mgpress ${⊢}\left({S}\in \mathrm{Ring}\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}={\mathrm{mulGrp}}_{{U}}$
18 16 17 sylan ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}={\mathrm{mulGrp}}_{{U}}$
19 18 oveq1d ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({\mathrm{mulGrp}}_{{S}}{↾}_{𝑠}{X}\right)\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}={\mathrm{mulGrp}}_{{U}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}$
20 15 19 eleqtrd ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left({\mathrm{mulGrp}}_{{U}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)$
21 8 20 jca ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to \left({{F}↾}_{{X}}\in \left({U}\mathrm{GrpHom}{T}\right)\wedge {{F}↾}_{{X}}\in \left({\mathrm{mulGrp}}_{{U}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)\right)$
22 eqid ${⊢}{\mathrm{mulGrp}}_{{U}}={\mathrm{mulGrp}}_{{U}}$
23 22 10 isrhm ${⊢}{{F}↾}_{{X}}\in \left({U}\mathrm{RingHom}{T}\right)↔\left(\left({U}\in \mathrm{Ring}\wedge {T}\in \mathrm{Ring}\right)\wedge \left({{F}↾}_{{X}}\in \left({U}\mathrm{GrpHom}{T}\right)\wedge {{F}↾}_{{X}}\in \left({\mathrm{mulGrp}}_{{U}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{T}}\right)\right)\right)$
24 4 21 23 sylanbrc ${⊢}\left({F}\in \left({S}\mathrm{RingHom}{T}\right)\wedge {X}\in \mathrm{SubRing}\left({S}\right)\right)\to {{F}↾}_{{X}}\in \left({U}\mathrm{RingHom}{T}\right)$