rhmimasubrng

Description: The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		rhmghm	$⊢ F \in (M RingHom N) \to F \in (M GrpHom N)$
2		subrngsubg	$⊢ X \in SubRng (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 SubRng (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		simpl	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to F \in ({mulGrp}_{M} MndHom {mulGrp}_{N})$
9		eqid	$⊢ {Base}_{M} = {Base}_{M}$
10	5 9	mgpbas	$⊢ {Base}_{M} = {Base}_{{mulGrp}_{M}}$
11	10	eqcomi	$⊢ {Base}_{{mulGrp}_{M}} = {Base}_{M}$
12	11	subrngss	$⊢ X \in SubRng (M) \to X \subseteq {Base}_{{mulGrp}_{M}}$
13	12	adantl	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to X \subseteq {Base}_{{mulGrp}_{M}}$
14		eqidd	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to +_{{mulGrp}_{M}} = +_{{mulGrp}_{M}}$
15		eqidd	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to +_{{mulGrp}_{N}} = +_{{mulGrp}_{N}}$
16		eqid	$⊢ \cdot_{M} = \cdot_{M}$
17	5 16	mgpplusg	$⊢ \cdot_{M} = +_{{mulGrp}_{M}}$
18	17	eqcomi	$⊢ +_{{mulGrp}_{M}} = \cdot_{M}$
19	18	subrngmcl	$⊢ (X \in SubRng (M) \land z \in X \land x \in X) \to z +_{{mulGrp}_{M}} x \in X$
20	19	3adant1l	$⊢ ((F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \land z \in X \land x \in X) \to z +_{{mulGrp}_{M}} x \in X$
21	8 13 14 15 20	mhmimalem	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to \forall x \in F [X] \forall y \in F [X] x +_{{mulGrp}_{N}} y \in F [X]$
22		eqid	$⊢ \cdot_{N} = \cdot_{N}$
23	6 22	mgpplusg	$⊢ \cdot_{N} = +_{{mulGrp}_{N}}$
24	23	eqcomi	$⊢ +_{{mulGrp}_{N}} = \cdot_{N}$
25	24	oveqi	$⊢ x +_{{mulGrp}_{N}} y = x \cdot_{N} y$
26	25	eleq1i	$⊢ x +_{{mulGrp}_{N}} y \in F [X] \leftrightarrow x \cdot_{N} y \in F [X]$
27	26	2ralbii	$⊢ \forall x \in F [X] \forall y \in F [X] x +_{{mulGrp}_{N}} y \in F [X] \leftrightarrow \forall x \in F [X] \forall y \in F [X] x \cdot_{N} y \in F [X]$
28	21 27	sylib	$⊢ (F \in ({mulGrp}_{M} MndHom {mulGrp}_{N}) \land X \in SubRng (M)) \to \forall x \in F [X] \forall y \in F [X] x \cdot_{N} y \in F [X]$
29	7 28	sylan	$⊢ (F \in (M RingHom N) \land X \in SubRng (M)) \to \forall x \in F [X] \forall y \in F [X] x \cdot_{N} y \in F [X]$
30		rhmrcl2	$⊢ F \in (M RingHom N) \to N \in Ring$
31		ringrng	$⊢ N \in Ring \to N \in Rng$
32	30 31	syl	$⊢ F \in (M RingHom N) \to N \in Rng$
33	32	adantr	$⊢ (F \in (M RingHom N) \land X \in SubRng (M)) \to N \in Rng$
34		eqid	$⊢ {Base}_{N} = {Base}_{N}$
35	34 22	issubrng2	$⊢ N \in Rng \to (F [X] \in SubRng (N) \leftrightarrow (F [X] \in SubGrp (N) \land \forall x \in F [X] \forall y \in F [X] x \cdot_{N} y \in F [X]))$
36	33 35	syl	$⊢ (F \in (M RingHom N) \land X \in SubRng (M)) \to (F [X] \in SubRng (N) \leftrightarrow (F [X] \in SubGrp (N) \land \forall x \in F [X] \forall y \in F [X] x \cdot_{N} y \in F [X]))$
37	4 29 36	mpbir2and	$⊢ (F \in (M RingHom N) \land X \in SubRng (M)) \to F [X] \in SubRng (N)$

Metamath Proof Explorer

Theorem rhmimasubrng

Proof