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		eqid	$⊢ {Base}_{M} = {Base}_{M}$
2		eqid	$⊢ {Base}_{N} = {Base}_{N}$
3	1 2	rhmf	$⊢ F \in (M RingHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
4	3	ffnd	$⊢ F \in (M RingHom N) \to F Fn {Base}_{M}$
5		fnima	$⊢ F Fn {Base}_{M} \to F [{Base}_{M}] = ran F$
6	4 5	syl	$⊢ F \in (M RingHom N) \to F [{Base}_{M}] = ran F$
7		rhmrcl1	$⊢ F \in (M RingHom N) \to M \in Ring$
8	1	subrgid	$⊢ M \in Ring \to {Base}_{M} \in SubRing (M)$
9	7 8	syl	$⊢ F \in (M RingHom N) \to {Base}_{M} \in SubRing (M)$
10		rhmima	$⊢ (F \in (M RingHom N) \land {Base}_{M} \in SubRing (M)) \to F [{Base}_{M}] \in SubRing (N)$
11	9 10	mpdan	$⊢ F \in (M RingHom N) \to F [{Base}_{M}] \in SubRing (N)$
12	6 11	eqeltrrd	$⊢ F \in (M RingHom N) \to ran F \in SubRing (N)$

Metamath Proof Explorer