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 \in SubRing (T) \land ran F \subseteq X) \to (F \in (S RingHom T) \leftrightarrow F \in (S RingHom U))$

Proof

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

Metamath Proof Explorer

Theorem resrhm2b

Proof