rhmimaidl

Description: The image of an ideal I by a surjective ring homomorphism F is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024)

	Ref	Expression
Hypotheses	rhmimaidl.b	$⊢ B = {Base}_{S}$
	rhmimaidl.t	$⊢ T = LIdeal (R)$
	rhmimaidl.u	$⊢ U = LIdeal (S)$
Assertion	rhmimaidl	$⊢ (F \in (R RingHom S) \land ran F = B \land I \in T) \to F [I] \in U$

Proof

Step	Hyp	Ref	Expression
1		rhmimaidl.b	$⊢ B = {Base}_{S}$
2		rhmimaidl.t	$⊢ T = LIdeal (R)$
3		rhmimaidl.u	$⊢ U = LIdeal (S)$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4 1	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ B$
6		fimass	$⊢ F : {Base}_{R} ⟶ B \to F [I] \subseteq B$
7	5 6	syl	$⊢ F \in (R RingHom S) \to F [I] \subseteq B$
8	7	ad2antrr	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F [I] \subseteq B$
9	5	ffnd	$⊢ F \in (R RingHom S) \to F Fn {Base}_{R}$
10	9	ad2antrr	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F Fn {Base}_{R}$
11		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
12	11	ad2antrr	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to R \in Ring$
13		eqid	$⊢ 0_{R} = 0_{R}$
14	4 13	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
15	12 14	syl	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to 0_{R} \in {Base}_{R}$
16		simpr	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to I \in T$
17	2 13	lidl0cl	$⊢ (R \in Ring \land I \in T) \to 0_{R} \in I$
18	12 16 17	syl2anc	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to 0_{R} \in I$
19	10 15 18	fnfvimad	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F (0_{R}) \in F [I]$
20	19	ne0d	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F [I] \neq \emptyset$
21		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
22	21	ad4antr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F \in (R GrpHom S)$
23	11	ad4antr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to R \in Ring$
24		simpr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to z \in {Base}_{R}$
25	4 2	lidlss	$⊢ I \in T \to I \subseteq {Base}_{R}$
26	25	ad4antlr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to I \subseteq {Base}_{R}$
27		simplr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to i \in I$
28	26 27	sseldd	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to i \in {Base}_{R}$
29		eqid	$⊢ \cdot_{R} = \cdot_{R}$
30	4 29	ringcl	$⊢ (R \in Ring \land z \in {Base}_{R} \land i \in {Base}_{R}) \to z \cdot_{R} i \in {Base}_{R}$
31	23 24 28 30	syl3anc	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to z \cdot_{R} i \in {Base}_{R}$
32		simpllr	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to j \in I$
33	26 32	sseldd	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to j \in {Base}_{R}$
34		eqid	$⊢ +_{R} = +_{R}$
35		eqid	$⊢ +_{S} = +_{S}$
36	4 34 35	ghmlin	$⊢ (F \in (R GrpHom S) \land z \cdot_{R} i \in {Base}_{R} \land j \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = F (z \cdot_{R} i) +_{S} F (j)$
37	22 31 33 36	syl3anc	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = F (z \cdot_{R} i) +_{S} F (j)$
38		simp-4l	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F \in (R RingHom S)$
39		eqid	$⊢ \cdot_{S} = \cdot_{S}$
40	4 29 39	rhmmul	$⊢ (F \in (R RingHom S) \land z \in {Base}_{R} \land i \in {Base}_{R}) \to F (z \cdot_{R} i) = F (z) \cdot_{S} F (i)$
41	38 24 28 40	syl3anc	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F (z \cdot_{R} i) = F (z) \cdot_{S} F (i)$
42	41	oveq1d	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F (z \cdot_{R} i) +_{S} F (j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
43	37 42	eqtrd	$⊢ ((((F \in (R RingHom S) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
44	43	adantl4r	$⊢ (((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
45	44	adantl3r	$⊢ ((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
46	45	adantl3r	$⊢ (((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
47	46	adantl3r	$⊢ ((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
48	47	adantllr	$⊢ (((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land z \in {Base}_{R}) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
49	48	ad4ant13	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F ((z \cdot_{R} i) +_{R} j) = (F (z) \cdot_{S} F (i)) +_{S} F (j)$
50		simpr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F (z) = x$
51		simpllr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F (i) = a$
52	50 51	oveq12d	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F (z) \cdot_{S} F (i) = x \cdot_{S} a$
53		simp-5r	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F (j) = b$
54	52 53	oveq12d	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to (F (z) \cdot_{S} F (i)) +_{S} F (j) = (x \cdot_{S} a) +_{S} b$
55	49 54	eqtrd	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F ((z \cdot_{R} i) +_{R} j) = (x \cdot_{S} a) +_{S} b$
56	10	ad9antr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F Fn {Base}_{R}$
57	16 25	syl	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to I \subseteq {Base}_{R}$
58	57	ad9antr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to I \subseteq {Base}_{R}$
59	16	ad9antr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to I \in T$
60		simplr	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to z \in {Base}_{R}$
61		simp-4r	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to i \in I$
62		simp-6r	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to j \in I$
63	2 4 34 29	islidl	$⊢ I \in T \leftrightarrow (I \subseteq {Base}_{R} \land I \neq \emptyset \land \forall z \in {Base}_{R} \forall i \in I \forall j \in I (z \cdot_{R} i) +_{R} j \in I)$
64	63	simp3bi	$⊢ I \in T \to \forall z \in {Base}_{R} \forall i \in I \forall j \in I (z \cdot_{R} i) +_{R} j \in I$
65	64	r19.21bi	$⊢ (I \in T \land z \in {Base}_{R}) \to \forall i \in I \forall j \in I (z \cdot_{R} i) +_{R} j \in I$
66	65	r19.21bi	$⊢ ((I \in T \land z \in {Base}_{R}) \land i \in I) \to \forall j \in I (z \cdot_{R} i) +_{R} j \in I$
67	66	r19.21bi	$⊢ (((I \in T \land z \in {Base}_{R}) \land i \in I) \land j \in I) \to (z \cdot_{R} i) +_{R} j \in I$
68	59 60 61 62 67	syl1111anc	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to (z \cdot_{R} i) +_{R} j \in I$
69	58 68	sseldd	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to (z \cdot_{R} i) +_{R} j \in {Base}_{R}$
70	56 69 68	fnfvimad	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to F ((z \cdot_{R} i) +_{R} j) \in F [I]$
71	55 70	eqeltrrd	$⊢ (((((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \land z \in {Base}_{R}) \land F (z) = x) \to (x \cdot_{S} a) +_{S} b \in F [I]$
72	5	ad2antrr	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F : {Base}_{R} ⟶ B$
73	72	ffund	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to Fun F$
74	73	ad7antr	$⊢ (((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \to Fun F$
75	5	fdmd	$⊢ F \in (R RingHom S) \to dom F = {Base}_{R}$
76	75	imaeq2d	$⊢ F \in (R RingHom S) \to F [dom F] = F [{Base}_{R}]$
77		imadmrn	$⊢ F [dom F] = ran F$
78	76 77	eqtr3di	$⊢ F \in (R RingHom S) \to F [{Base}_{R}] = ran F$
79	78	eqeq1d	$⊢ F \in (R RingHom S) \to (F [{Base}_{R}] = B \leftrightarrow ran F = B)$
80	79	biimpar	$⊢ (F \in (R RingHom S) \land ran F = B) \to F [{Base}_{R}] = B$
81	80	eleq2d	$⊢ (F \in (R RingHom S) \land ran F = B) \to (x \in F [{Base}_{R}] \leftrightarrow x \in B)$
82	81	biimpar	$⊢ ((F \in (R RingHom S) \land ran F = B) \land x \in B) \to x \in F [{Base}_{R}]$
83	82	adantlr	$⊢ (((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \to x \in F [{Base}_{R}]$
84	83	ad6antr	$⊢ (((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \to x \in F [{Base}_{R}]$
85		fvelima	$⊢ (Fun F \land x \in F [{Base}_{R}]) \to \exists z \in {Base}_{R} F (z) = x$
86	74 84 85	syl2anc	$⊢ (((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \to \exists z \in {Base}_{R} F (z) = x$
87	71 86	r19.29a	$⊢ (((((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \land i \in I) \land F (i) = a) \to (x \cdot_{S} a) +_{S} b \in F [I]$
88	73	ad5antr	$⊢ (((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \to Fun F$
89		simp-4r	$⊢ (((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \to a \in F [I]$
90		fvelima	$⊢ (Fun F \land a \in F [I]) \to \exists i \in I F (i) = a$
91	88 89 90	syl2anc	$⊢ (((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \to \exists i \in I F (i) = a$
92	87 91	r19.29a	$⊢ (((((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \land j \in I) \land F (j) = b) \to (x \cdot_{S} a) +_{S} b \in F [I]$
93	73	ad3antrrr	$⊢ (((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \to Fun F$
94		simpr	$⊢ (((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \to b \in F [I]$
95		fvelima	$⊢ (Fun F \land b \in F [I]) \to \exists j \in I F (j) = b$
96	93 94 95	syl2anc	$⊢ (((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \to \exists j \in I F (j) = b$
97	92 96	r19.29a	$⊢ (((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land a \in F [I]) \land b \in F [I]) \to (x \cdot_{S} a) +_{S} b \in F [I]$
98	97	anasss	$⊢ ((((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \land (a \in F [I] \land b \in F [I])) \to (x \cdot_{S} a) +_{S} b \in F [I]$
99	98	ralrimivva	$⊢ (((F \in (R RingHom S) \land ran F = B) \land I \in T) \land x \in B) \to \forall a \in F [I] \forall b \in F [I] (x \cdot_{S} a) +_{S} b \in F [I]$
100	99	ralrimiva	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to \forall x \in B \forall a \in F [I] \forall b \in F [I] (x \cdot_{S} a) +_{S} b \in F [I]$
101	3 1 35 39	islidl	$⊢ F [I] \in U \leftrightarrow (F [I] \subseteq B \land F [I] \neq \emptyset \land \forall x \in B \forall a \in F [I] \forall b \in F [I] (x \cdot_{S} a) +_{S} b \in F [I])$
102	8 20 100 101	syl3anbrc	$⊢ ((F \in (R RingHom S) \land ran F = B) \land I \in T) \to F [I] \in U$
103	102	3impa	$⊢ (F \in (R RingHom S) \land ran F = B \land I \in T) \to F [I] \in U$

Metamath Proof Explorer

Theorem rhmimaidl

Proof