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 ) ) )