Theorem rhmimasubrng

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

	Ref	Expression
Assertion	rhmimasubrng	Could not format assertion : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubRng ` N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rhmghm	$$⊢F\in \left(M\mathrm{RingHom}N\right)\to F\in \left(M\mathrm{GrpHom}N\right)$$
2		subrngsubg	Could not format ( X e. ( SubRng ` M ) -> X e. ( SubGrp ` M ) ) : No typesetting found for |- ( X e. ( SubRng ` M ) -> X e. ( SubGrp ` M ) ) with typecode |-
3		ghmima	$$⊢\left(F\in \left(M\mathrm{GrpHom}N\right)\wedge X\in \mathrm{SubGrp}\left(M\right)\right)\to F\left[X\right]\in \mathrm{SubGrp}\left(N\right)$$
4	1 2 3	syl2an	Could not format ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubGrp ` N ) ) : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubGrp ` N ) ) with typecode |-
5		eqid	$$⊢{\mathrm{mulGrp}}_M={\mathrm{mulGrp}}_M$$
6		eqid	$$⊢{\mathrm{mulGrp}}_N={\mathrm{mulGrp}}_N$$
7	5 6	rhmmhm	$$⊢F\in \left(M\mathrm{RingHom}N\right)\to F\in \left({\mathrm{mulGrp}}_M\mathrm{MndHom}{\mathrm{mulGrp}}_N\right)$$
8		simpl	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) ) with typecode |-
9		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
10	5 9	mgpbas	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_{{\mathrm{mulGrp}}_M}$$
11	10	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_M}={\mathrm{Base}}_M$$
12	11	subrngss	Could not format ( X e. ( SubRng ` M ) -> X C_ ( Base ` ( mulGrp ` M ) ) ) : No typesetting found for |- ( X e. ( SubRng ` M ) -> X C_ ( Base ` ( mulGrp ` M ) ) ) with typecode |-
13	12	adantl	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> X C_ ( Base ` ( mulGrp ` M ) ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> X C_ ( Base ` ( mulGrp ` M ) ) ) with typecode |-
14		eqidd	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` M ) ) = ( +g ` ( mulGrp ` M ) ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` M ) ) = ( +g ` ( mulGrp ` M ) ) ) with typecode |-
15		eqidd	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` N ) ) = ( +g ` ( mulGrp ` N ) ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` N ) ) = ( +g ` ( mulGrp ` N ) ) ) with typecode |-
16		eqid	$$⊢{\cdot }_M={\cdot }_M$$
17	5 16	mgpplusg	$$⊢{\cdot }_M={+}_{{\mathrm{mulGrp}}_M}$$
18	17	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_M}={\cdot }_M$$
19	18	subrngmcl	Could not format ( ( X e. ( SubRng ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X ) : No typesetting found for |- ( ( X e. ( SubRng ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X ) with typecode |-
20	19	3adant1l	Could not format ( ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X ) : No typesetting found for |- ( ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X ) with typecode |-
21	8 13 14 15 20	mhmimalem	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` ( mulGrp ` N ) ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` ( mulGrp ` N ) ) y ) e. ( F " X ) ) with typecode |-
22		eqid	$$⊢{\cdot }_N={\cdot }_N$$
23	6 22	mgpplusg	$$⊢{\cdot }_N={+}_{{\mathrm{mulGrp}}_N}$$
24	23	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_N}={\cdot }_N$$
25	24	oveqi	$$⊢x{+}_{{\mathrm{mulGrp}}_N}y=x{\cdot }_{N}y$$
26	25	eleq1i	$$⊢x{+}_{{\mathrm{mulGrp}}_N}y\in F\left[X\right]\leftrightarrow x{\cdot }_{N}y\in F\left[X\right]$$
27	26	2ralbii	$$⊢\forall x\in F\left[X\right]\forall y\in F\left[X\right]x{+}_{{\mathrm{mulGrp}}_N}y\in F\left[X\right]\leftrightarrow \forall x\in F\left[X\right]\forall y\in F\left[X\right]x{\cdot }_{N}y\in F\left[X\right]$$
28	21 27	sylib	Could not format ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) with typecode |-
29	7 28	sylan	Could not format ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) with typecode |-
30		rhmrcl2	$$⊢F\in \left(M\mathrm{RingHom}N\right)\to N\in \mathrm{Ring}$$
31		ringrng	$$⊢N\in \mathrm{Ring}\to N\in \mathrm{Rng}$$
32	30 31	syl	$$⊢F\in \left(M\mathrm{RingHom}N\right)\to N\in \mathrm{Rng}$$
33	32	adantr	Could not format ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> N e. Rng ) : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> N e. Rng ) with typecode |-
34		eqid	$$⊢{\mathrm{Base}}_N={\mathrm{Base}}_N$$
35	34 22	issubrng2	Could not format ( N e. Rng -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) ) : No typesetting found for |- ( N e. Rng -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) ) with typecode |-
36	33 35	syl	Could not format ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) ) : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) ) with typecode |-
37	4 29 36	mpbir2and	Could not format ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubRng ` N ) ) : No typesetting found for |- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubRng ` N ) ) with typecode |-