rhmima

Description: The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	rhmima	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to F [X] \in SubRing (N)$

Step	Hyp	Ref	Expression
1		rhmghm	$⊢ F \in (M RingHom N) \to F \in (M GrpHom N)$
2		subrgsubg	$⊢ X \in SubRing (M) \to X \in SubGrp (M)$
3		ghmima	$⊢ (F \in (M GrpHom N) \land X \in SubGrp (M)) \to F [X] \in SubGrp (N)$
4	1 2 3	syl2an	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to F [X] \in SubGrp (N)$
5		eqid	$⊢ {mulGrp}_{M} = {mulGrp}_{M}$
6		eqid	$⊢ {mulGrp}_{N} = {mulGrp}_{N}$
7	5 6	rhmmhm	$⊢ F \in (M RingHom N) \to F \in ({mulGrp}_{M} MndHom {mulGrp}_{N})$
8	5	subrgsubm	$⊢ X \in SubRing (M) \to X \in SubMnd ({mulGrp}_{M})$
9		mhmima	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubMnd ({mulGrp}_{M})) \to F [X] \in SubMnd ({mulGrp}_{N})$
10	7 8 9	syl2an	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to F [X] \in SubMnd ({mulGrp}_{N})$
11		rhmrcl2	$⊢ F \in (M RingHom N) \to N \in Ring$
12	11	adantr	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to N \in Ring$
13	6	issubrg3	$⊢ N \in Ring \to (F [X] \in SubRing (N) \leftrightarrow (F [X] \in SubGrp (N) \land F [X] \in SubMnd ({mulGrp}_{N})))$
14	12 13	syl	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to (F [X] \in SubRing (N) \leftrightarrow (F [X] \in SubGrp (N) \land F [X] \in SubMnd ({mulGrp}_{N})))$
15	4 10 14	mpbir2and	$⊢ (F \in (M RingHom N) \land X \in SubRing (M)) \to F [X] \in SubRing (N)$

Metamath Proof Explorer