imacrhmcl

Description: The image of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025)

	Ref	Expression
Hypotheses	imacrhmcl.c	$⊢ C = N ↾_{𝑠} F [S]$
	imacrhmcl.h	$⊢ φ \to F \in (M RingHom N)$
	imacrhmcl.m	$⊢ φ \to M \in CRing$
	imacrhmcl.s	$⊢ φ \to S \in SubRing (M)$
Assertion	imacrhmcl	$⊢ φ \to C \in CRing$

Proof

Step	Hyp	Ref	Expression
1		imacrhmcl.c	$⊢ C = N ↾_{𝑠} F [S]$
2		imacrhmcl.h	$⊢ φ \to F \in (M RingHom N)$
3		imacrhmcl.m	$⊢ φ \to M \in CRing$
4		imacrhmcl.s	$⊢ φ \to S \in SubRing (M)$
5		rhmima	$⊢ (F \in (M RingHom N) \land S \in SubRing (M)) \to F [S] \in SubRing (N)$
6	2 4 5	syl2anc	$⊢ φ \to F [S] \in SubRing (N)$
7	1	subrgring	$⊢ F [S] \in SubRing (N) \to C \in Ring$
8	6 7	syl	$⊢ φ \to C \in Ring$
9	1	ressbasss2	$⊢ {Base}_{C} \subseteq F [S]$
10	9	sseli	$⊢ x \in {Base}_{C} \to x \in F [S]$
11	9	sseli	$⊢ y \in {Base}_{C} \to y \in F [S]$
12	10 11	anim12i	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to (x \in F [S] \land y \in F [S])$
13		eqid	$⊢ {Base}_{M} = {Base}_{M}$
14		eqid	$⊢ {Base}_{N} = {Base}_{N}$
15	13 14	rhmf	$⊢ F \in (M RingHom N) \to F : {Base}_{M} ⟶ {Base}_{N}$
16	2 15	syl	$⊢ φ \to F : {Base}_{M} ⟶ {Base}_{N}$
17	16	ffund	$⊢ φ \to Fun F$
18		fvelima	$⊢ (Fun F \land x \in F [S]) \to \exists a \in S F (a) = x$
19	17 18	sylan	$⊢ (φ \land x \in F [S]) \to \exists a \in S F (a) = x$
20	19	adantrr	$⊢ (φ \land (x \in F [S] \land y \in F [S])) \to \exists a \in S F (a) = x$
21		fvelima	$⊢ (Fun F \land y \in F [S]) \to \exists b \in S F (b) = y$
22	17 21	sylan	$⊢ (φ \land y \in F [S]) \to \exists b \in S F (b) = y$
23	22	adantrl	$⊢ (φ \land (x \in F [S] \land y \in F [S])) \to \exists b \in S F (b) = y$
24	23	adantr	$⊢ ((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \to \exists b \in S F (b) = y$
25	3	ad3antrrr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to M \in CRing$
26	13	subrgss	$⊢ S \in SubRing (M) \to S \subseteq {Base}_{M}$
27	4 26	syl	$⊢ φ \to S \subseteq {Base}_{M}$
28	27	ad3antrrr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to S \subseteq {Base}_{M}$
29		simplrl	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to a \in S$
30	28 29	sseldd	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to a \in {Base}_{M}$
31		simprl	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to b \in S$
32	28 31	sseldd	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to b \in {Base}_{M}$
33		eqid	$⊢ \cdot_{M} = \cdot_{M}$
34	13 33	crngcom	$⊢ (M \in CRing \land a \in {Base}_{M} \land b \in {Base}_{M}) \to a \cdot_{M} b = b \cdot_{M} a$
35	25 30 32 34	syl3anc	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to a \cdot_{M} b = b \cdot_{M} a$
36	35	fveq2d	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (a \cdot_{M} b) = F (b \cdot_{M} a)$
37	2	ad3antrrr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F \in (M RingHom N)$
38		eqid	$⊢ \cdot_{N} = \cdot_{N}$
39	13 33 38	rhmmul	$⊢ (F \in (M RingHom N) \land a \in {Base}_{M} \land b \in {Base}_{M}) \to F (a \cdot_{M} b) = F (a) \cdot_{N} F (b)$
40	37 30 32 39	syl3anc	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (a \cdot_{M} b) = F (a) \cdot_{N} F (b)$
41	13 33 38	rhmmul	$⊢ (F \in (M RingHom N) \land b \in {Base}_{M} \land a \in {Base}_{M}) \to F (b \cdot_{M} a) = F (b) \cdot_{N} F (a)$
42	37 32 30 41	syl3anc	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (b \cdot_{M} a) = F (b) \cdot_{N} F (a)$
43	36 40 42	3eqtr3d	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (a) \cdot_{N} F (b) = F (b) \cdot_{N} F (a)$
44		imaexg	$⊢ F \in (M RingHom N) \to F [S] \in V$
45	1 38	ressmulr	$⊢ F [S] \in V \to \cdot_{N} = \cdot_{C}$
46	2 44 45	3syl	$⊢ φ \to \cdot_{N} = \cdot_{C}$
47	46	ad3antrrr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to \cdot_{N} = \cdot_{C}$
48		simplrr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (a) = x$
49		simprr	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (b) = y$
50	47 48 49	oveq123d	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (a) \cdot_{N} F (b) = x \cdot_{C} y$
51	47 49 48	oveq123d	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to F (b) \cdot_{N} F (a) = y \cdot_{C} x$
52	43 50 51	3eqtr3d	$⊢ (((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \land (b \in S \land F (b) = y)) \to x \cdot_{C} y = y \cdot_{C} x$
53	24 52	rexlimddv	$⊢ ((φ \land (x \in F [S] \land y \in F [S])) \land (a \in S \land F (a) = x)) \to x \cdot_{C} y = y \cdot_{C} x$
54	20 53	rexlimddv	$⊢ (φ \land (x \in F [S] \land y \in F [S])) \to x \cdot_{C} y = y \cdot_{C} x$
55	12 54	sylan2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \cdot_{C} y = y \cdot_{C} x$
56	55	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x$
57		eqid	$⊢ {Base}_{C} = {Base}_{C}$
58		eqid	$⊢ \cdot_{C} = \cdot_{C}$
59	57 58	iscrng2	$⊢ C \in CRing \leftrightarrow (C \in Ring \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} x \cdot_{C} y = y \cdot_{C} x)$
60	8 56 59	sylanbrc	$⊢ φ \to C \in CRing$

Metamath Proof Explorer

Theorem imacrhmcl

Proof