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 ⊢ F ∈ S RingHom T ∧ X ∈ SubRing ⁡ S → F ↾ X ∈ U RingHom T

Proof

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