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 ↾ 𝑠 X
Assertion resrhm2b ⊢ X ∈ SubRing ⁡ T ∧ ran ⁡ F ⊆ X → F ∈ S RingHom T ↔ F ∈ S RingHom U

Proof

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