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 ⊢ 𝑈 = ( 𝑆 ↾s 𝑋 )
Assertion resrhm ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 RingHom 𝑇 ) )

Proof

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