Metamath Proof Explorer

Theorem resrhm2b

Description: Restriction of the codomain of a (ring) homomorphism. resghm2b analog. (Contributed by SN, 7-Feb-2025)

Ref Expression
Hypothesis resrhm2b.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
Assertion resrhm2b ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 RingHom 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 resrhm2b.u ⊢ 𝑈 = ( 𝑇 ↾s 𝑋 )
2 subrgsubg ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) → 𝑋 ∈ ( SubGrp ‘ 𝑇 ) )
3 1 resghm2b ⊢ ( ( 𝑋 ∈ ( SubGrp ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
4 2 3 sylan ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ) )
5 eqid ⊢ ( mulGrp ‘ 𝑇 ) = ( mulGrp ‘ 𝑇 )
6 5 subrgsubm ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) → 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑇 ) ) )
7 eqid ⊢ ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) = ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 )
8 7 resmhm2b ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑇 ) ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ↔ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) ) ) )
9 6 8 sylan ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ↔ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) ) ) )
10 subrgrcl ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) → 𝑇 ∈ Ring )
11 1 5 mgpress ⊢ ( ( 𝑇 ∈ Ring ∧ 𝑋 ∈ ( SubRing ‘ 𝑇 ) ) → ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) = ( mulGrp ‘ 𝑈 ) )
12 10 11 mpancom ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) → ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) = ( mulGrp ‘ 𝑈 ) )
13 12 adantr ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) = ( mulGrp ‘ 𝑈 ) )
14 13 oveq2d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( mulGrp ‘ 𝑆 ) MndHom ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) ) = ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) )
15 14 eleq2d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( ( mulGrp ‘ 𝑇 ) ↾s 𝑋 ) ) ↔ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
16 9 15 bitrd ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ↔ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) )
17 4 16 anbi12d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) )
18 17 anbi2d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) ↔ ( 𝑆 ∈ Ring ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) ) )
19 10 adantr ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → 𝑇 ∈ Ring )
20 19 biantrud ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝑆 ∈ Ring ↔ ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) ) )
21 20 anbi1d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) ) )
22 1 subrgring ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) → 𝑈 ∈ Ring )
23 22 adantr ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → 𝑈 ∈ Ring )
24 23 biantrud ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝑆 ∈ Ring ↔ ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) ) )
25 24 anbi1d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) ) )
26 18 21 25 3bitr3d ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) ) )
27 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
28 27 5 isrhm ⊢ ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑇 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑇 ) ) ) ) )
29 eqid ⊢ ( mulGrp ‘ 𝑈 ) = ( mulGrp ‘ 𝑈 )
30 27 29 isrhm ⊢ ( 𝐹 ∈ ( 𝑆 RingHom 𝑈 ) ↔ ( ( 𝑆 ∈ Ring ∧ 𝑈 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑈 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑆 ) MndHom ( mulGrp ‘ 𝑈 ) ) ) ) )
31 26 28 30 3bitr4g ⊢ ( ( 𝑋 ∈ ( SubRing ‘ 𝑇 ) ∧ ran 𝐹 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ↔ 𝐹 ∈ ( 𝑆 RingHom 𝑈 ) ) )