rnrhmsubrg

Description: The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023)

		Ref	Expression
	Assertion	rnrhmsubrg	$⊢ F \in (M RingHom N) \to ran F \in SubRing (N)$

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [{Base}_{M}] = ran ({F ↾}_{{Base}_{M}})$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ {Base}_{N} = {Base}_{N}$
4	2 3	rhmf	$⊢ F \in (M RingHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
5	4	ffnd	$⊢ F \in (M RingHom N) \to F Fn {Base}_{M}$
6		fnresdm	$⊢ F Fn {Base}_{M} \to {F ↾}_{{Base}_{M}} = F$
7	5 6	syl	$⊢ F \in (M RingHom N) \to {F ↾}_{{Base}_{M}} = F$
8	7	rneqd	$⊢ F \in (M RingHom N) \to ran ({F ↾}_{{Base}_{M}}) = ran F$
9	1 8	eqtr2id	$⊢ F \in (M RingHom N) \to ran F = F [{Base}_{M}]$
10		rhmrcl1	$⊢ F \in (M RingHom N) \to M \in Ring$
11	2	subrgid	$⊢ M \in Ring \to {Base}_{M} \in SubRing (M)$
12	10 11	syl	$⊢ F \in (M RingHom N) \to {Base}_{M} \in SubRing (M)$
13		rhmima	$⊢ (F \in (M RingHom N) \land {Base}_{M} \in SubRing (M)) \to F [{Base}_{M}] \in SubRing (N)$
14	12 13	mpdan	$⊢ F \in (M RingHom N) \to F [{Base}_{M}] \in SubRing (N)$
15	9 14	eqeltrd	$⊢ F \in (M RingHom N) \to ran F \in SubRing (N)$

Metamath Proof Explorer