rhmpreimaidl

Description: The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

		Ref	Expression
	Hypothesis	rhmpreimaidl.i	$⊢ I = LIdeal (R)$
	Assertion	rhmpreimaidl	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F^{-1} [J] \in I$

Proof

Step	Hyp	Ref	Expression
1		rhmpreimaidl.i	$⊢ I = LIdeal (R)$
2		cnvimass	$⊢ F^{-1} [J] \subseteq dom F$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5	3 4	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
6	2 5	fssdm	$⊢ F \in (R RingHom S) \to F^{-1} [J] \subseteq {Base}_{R}$
7	6	adantr	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F^{-1} [J] \subseteq {Base}_{R}$
8	5	adantr	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F : {Base}_{R} ⟶ {Base}_{S}$
9	8	ffund	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to Fun F$
10		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
11	10	adantr	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to R \in Ring$
12		eqid	$⊢ 0_{R} = 0_{R}$
13	3 12	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
14	11 13	syl	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to 0_{R} \in {Base}_{R}$
15	8	fdmd	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to dom F = {Base}_{R}$
16	14 15	eleqtrrd	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to 0_{R} \in dom F$
17		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
18		ghmmhm	$⊢ F \in (R GrpHom S) \to F \in (R MndHom S)$
19		eqid	$⊢ 0_{S} = 0_{S}$
20	12 19	mhm0	$⊢ F \in (R MndHom S) \to F (0_{R}) = 0_{S}$
21	17 18 20	3syl	$⊢ F \in (R RingHom S) \to F (0_{R}) = 0_{S}$
22	21	adantr	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F (0_{R}) = 0_{S}$
23		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
24		eqid	$⊢ LIdeal (S) = LIdeal (S)$
25	24 19	lidl0cl	$⊢ (S \in Ring \land J \in LIdeal (S)) \to 0_{S} \in J$
26	23 25	sylan	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to 0_{S} \in J$
27	22 26	eqeltrd	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F (0_{R}) \in J$
28		fvimacnv	$⊢ (Fun F \land 0_{R} \in dom F) \to (F (0_{R}) \in J \leftrightarrow 0_{R} \in F^{-1} [J])$
29	28	biimpa	$⊢ ((Fun F \land 0_{R} \in dom F) \land F (0_{R}) \in J) \to 0_{R} \in F^{-1} [J]$
30	9 16 27 29	syl21anc	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to 0_{R} \in F^{-1} [J]$
31	30	ne0d	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F^{-1} [J] \neq \emptyset$
32	8	ffnd	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F Fn {Base}_{R}$
33	32	ad3antrrr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F Fn {Base}_{R}$
34	11	ad3antrrr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to R \in Ring$
35		simpllr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to x \in {Base}_{R}$
36	6	ad2antrr	$⊢ ((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \to F^{-1} [J] \subseteq {Base}_{R}$
37	36	sselda	$⊢ (((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \to a \in {Base}_{R}$
38	37	adantr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to a \in {Base}_{R}$
39		eqid	$⊢ \cdot_{R} = \cdot_{R}$
40	3 39	ringcl	$⊢ (R \in Ring \land x \in {Base}_{R} \land a \in {Base}_{R}) \to x \cdot_{R} a \in {Base}_{R}$
41	34 35 38 40	syl3anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to x \cdot_{R} a \in {Base}_{R}$
42	36	adantr	$⊢ (((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \to F^{-1} [J] \subseteq {Base}_{R}$
43	42	sselda	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to b \in {Base}_{R}$
44		eqid	$⊢ +_{R} = +_{R}$
45	3 44	ringacl	$⊢ (R \in Ring \land x \cdot_{R} a \in {Base}_{R} \land b \in {Base}_{R}) \to (x \cdot_{R} a) +_{R} b \in {Base}_{R}$
46	34 41 43 45	syl3anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to (x \cdot_{R} a) +_{R} b \in {Base}_{R}$
47	17	ad4antr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F \in (R GrpHom S)$
48		eqid	$⊢ +_{S} = +_{S}$
49	3 44 48	ghmlin	$⊢ (F \in (R GrpHom S) \land x \cdot_{R} a \in {Base}_{R} \land b \in {Base}_{R}) \to F ((x \cdot_{R} a) +_{R} b) = F (x \cdot_{R} a) +_{S} F (b)$
50	47 41 43 49	syl3anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F ((x \cdot_{R} a) +_{R} b) = F (x \cdot_{R} a) +_{S} F (b)$
51		simp-4l	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F \in (R RingHom S)$
52	51 23	syl	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to S \in Ring$
53		simpr	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to J \in LIdeal (S)$
54	53	ad3antrrr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to J \in LIdeal (S)$
55		eqid	$⊢ \cdot_{S} = \cdot_{S}$
56	3 39 55	rhmmul	$⊢ (F \in (R RingHom S) \land x \in {Base}_{R} \land a \in {Base}_{R}) \to F (x \cdot_{R} a) = F (x) \cdot_{S} F (a)$
57	51 35 38 56	syl3anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (x \cdot_{R} a) = F (x) \cdot_{S} F (a)$
58	8	ffvelcdmda	$⊢ ((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \to F (x) \in {Base}_{S}$
59	58	ad2antrr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (x) \in {Base}_{S}$
60		simplr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to a \in F^{-1} [J]$
61		elpreima	$⊢ F Fn {Base}_{R} \to (a \in F^{-1} [J] \leftrightarrow (a \in {Base}_{R} \land F (a) \in J))$
62	61	simplbda	$⊢ (F Fn {Base}_{R} \land a \in F^{-1} [J]) \to F (a) \in J$
63	33 60 62	syl2anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (a) \in J$
64	24 4 55	lidlmcl	$⊢ ((S \in Ring \land J \in LIdeal (S)) \land (F (x) \in {Base}_{S} \land F (a) \in J)) \to F (x) \cdot_{S} F (a) \in J$
65	52 54 59 63 64	syl22anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (x) \cdot_{S} F (a) \in J$
66	57 65	eqeltrd	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (x \cdot_{R} a) \in J$
67		simpr	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to b \in F^{-1} [J]$
68		elpreima	$⊢ F Fn {Base}_{R} \to (b \in F^{-1} [J] \leftrightarrow (b \in {Base}_{R} \land F (b) \in J))$
69	68	simplbda	$⊢ (F Fn {Base}_{R} \land b \in F^{-1} [J]) \to F (b) \in J$
70	33 67 69	syl2anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (b) \in J$
71	24 48	lidlacl	$⊢ ((S \in Ring \land J \in LIdeal (S)) \land (F (x \cdot_{R} a) \in J \land F (b) \in J)) \to F (x \cdot_{R} a) +_{S} F (b) \in J$
72	52 54 66 70 71	syl22anc	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F (x \cdot_{R} a) +_{S} F (b) \in J$
73	50 72	eqeltrd	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to F ((x \cdot_{R} a) +_{R} b) \in J$
74	33 46 73	elpreimad	$⊢ ((((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land a \in F^{-1} [J]) \land b \in F^{-1} [J]) \to (x \cdot_{R} a) +_{R} b \in F^{-1} [J]$
75	74	anasss	$⊢ (((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \land (a \in F^{-1} [J] \land b \in F^{-1} [J])) \to (x \cdot_{R} a) +_{R} b \in F^{-1} [J]$
76	75	ralrimivva	$⊢ ((F \in (R RingHom S) \land J \in LIdeal (S)) \land x \in {Base}_{R}) \to \forall a \in F^{-1} [J] \forall b \in F^{-1} [J] (x \cdot_{R} a) +_{R} b \in F^{-1} [J]$
77	76	ralrimiva	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to \forall x \in {Base}_{R} \forall a \in F^{-1} [J] \forall b \in F^{-1} [J] (x \cdot_{R} a) +_{R} b \in F^{-1} [J]$
78	1 3 44 39	islidl	$⊢ F^{-1} [J] \in I \leftrightarrow (F^{-1} [J] \subseteq {Base}_{R} \land F^{-1} [J] \neq \emptyset \land \forall x \in {Base}_{R} \forall a \in F^{-1} [J] \forall b \in F^{-1} [J] (x \cdot_{R} a) +_{R} b \in F^{-1} [J])$
79	7 31 77 78	syl3anbrc	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F^{-1} [J] \in I$

Metamath Proof Explorer

Theorem rhmpreimaidl

Proof