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
|- U = ( T |`s X )
Assertion resrhm2b
|- ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( S RingHom T ) <-> F e. ( S RingHom U ) ) )

Proof

Step Hyp Ref Expression
1 resrhm2b.u
 |-  U = ( T |`s X )
2 subrgsubg
 |-  ( X e. ( SubRing ` T ) -> X e. ( SubGrp ` T ) )
3 1 resghm2b
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
4 2 3 sylan
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
5 eqid
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
6 5 subrgsubm
 |-  ( X e. ( SubRing ` T ) -> X e. ( SubMnd ` ( mulGrp ` T ) ) )
7 eqid
 |-  ( ( mulGrp ` T ) |`s X ) = ( ( mulGrp ` T ) |`s X )
8 7 resmhm2b
 |-  ( ( X e. ( SubMnd ` ( mulGrp ` T ) ) /\ ran F C_ X ) -> ( F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) <-> F e. ( ( mulGrp ` S ) MndHom ( ( mulGrp ` T ) |`s X ) ) ) )
9 6 8 sylan
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) <-> F e. ( ( mulGrp ` S ) MndHom ( ( mulGrp ` T ) |`s X ) ) ) )
10 subrgrcl
 |-  ( X e. ( SubRing ` T ) -> T e. Ring )
11 1 5 mgpress
 |-  ( ( T e. Ring /\ X e. ( SubRing ` T ) ) -> ( ( mulGrp ` T ) |`s X ) = ( mulGrp ` U ) )
12 10 11 mpancom
 |-  ( X e. ( SubRing ` T ) -> ( ( mulGrp ` T ) |`s X ) = ( mulGrp ` U ) )
13 12 adantr
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( mulGrp ` T ) |`s X ) = ( mulGrp ` U ) )
14 13 oveq2d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( mulGrp ` S ) MndHom ( ( mulGrp ` T ) |`s X ) ) = ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) )
15 14 eleq2d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( ( mulGrp ` S ) MndHom ( ( mulGrp ` T ) |`s X ) ) <-> F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) )
16 9 15 bitrd
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) <-> F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) )
17 4 16 anbi12d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) <-> ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) )
18 17 anbi2d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( S e. Ring /\ ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) <-> ( S e. Ring /\ ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) ) )
19 10 adantr
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> T e. Ring )
20 19 biantrud
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( S e. Ring <-> ( S e. Ring /\ T e. Ring ) ) )
21 20 anbi1d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( S e. Ring /\ ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) <-> ( ( S e. Ring /\ T e. Ring ) /\ ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) ) )
22 1 subrgring
 |-  ( X e. ( SubRing ` T ) -> U e. Ring )
23 22 adantr
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> U e. Ring )
24 23 biantrud
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( S e. Ring <-> ( S e. Ring /\ U e. Ring ) ) )
25 24 anbi1d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( S e. Ring /\ ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) <-> ( ( S e. Ring /\ U e. Ring ) /\ ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) ) )
26 18 21 25 3bitr3d
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( ( ( S e. Ring /\ T e. Ring ) /\ ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) <-> ( ( S e. Ring /\ U e. Ring ) /\ ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) ) )
27 eqid
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
28 27 5 isrhm
 |-  ( F e. ( S RingHom T ) <-> ( ( S e. Ring /\ T e. Ring ) /\ ( F e. ( S GrpHom T ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) ) ) )
29 eqid
 |-  ( mulGrp ` U ) = ( mulGrp ` U )
30 27 29 isrhm
 |-  ( F e. ( S RingHom U ) <-> ( ( S e. Ring /\ U e. Ring ) /\ ( F e. ( S GrpHom U ) /\ F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` U ) ) ) ) )
31 26 28 30 3bitr4g
 |-  ( ( X e. ( SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( S RingHom T ) <-> F e. ( S RingHom U ) ) )