rhmpreimaprmidl

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

		Ref	Expression
	Hypothesis	rhmpreimaprmidl.p	$⊢ P = PrmIdeal (R)$
	Assertion	rhmpreimaprmidl	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to F^{-1} [J] \in P$

Proof

Step	Hyp	Ref	Expression
1		rhmpreimaprmidl.p	$⊢ P = PrmIdeal (R)$
2		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
3	2	ad2antlr	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to R \in Ring$
4		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
5		prmidlidl	$⊢ (S \in Ring \land J \in PrmIdeal (S)) \to J \in LIdeal (S)$
6	4 5	sylan	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to J \in LIdeal (S)$
7		eqid	$⊢ LIdeal (R) = LIdeal (R)$
8	7	rhmpreimaidl	$⊢ (F \in (R RingHom S) \land J \in LIdeal (S)) \to F^{-1} [J] \in LIdeal (R)$
9	6 8	syldan	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to F^{-1} [J] \in LIdeal (R)$
10	9	adantll	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to F^{-1} [J] \in LIdeal (R)$
11	4	adantr	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to S \in Ring$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13		eqid	$⊢ \cdot_{S} = \cdot_{S}$
14	12 13	prmidlnr	$⊢ (S \in Ring \land J \in PrmIdeal (S)) \to J \neq {Base}_{S}$
15	4 14	sylan	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to J \neq {Base}_{S}$
16		eqid	$⊢ 1_{S} = 1_{S}$
17	12 16	pridln1	$⊢ (S \in Ring \land J \in LIdeal (S) \land J \neq {Base}_{S}) \to \neg 1_{S} \in J$
18	11 6 15 17	syl3anc	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to \neg 1_{S} \in J$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	19 16	rhm1	$⊢ F \in (R RingHom S) \to F (1_{R}) = 1_{S}$
21	20	ad2antrr	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to F (1_{R}) = 1_{S}$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23	22 12	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
24	23	ffnd	$⊢ F \in (R RingHom S) \to F Fn {Base}_{R}$
25	24	ad2antrr	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to F Fn {Base}_{R}$
26	22 19	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
27	2 26	syl	$⊢ F \in (R RingHom S) \to 1_{R} \in {Base}_{R}$
28	27	ad2antrr	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to 1_{R} \in {Base}_{R}$
29		simpr	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to F^{-1} [J] = {Base}_{R}$
30	28 29	eleqtrrd	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to 1_{R} \in F^{-1} [J]$
31		elpreima	$⊢ F Fn {Base}_{R} \to (1_{R} \in F^{-1} [J] \leftrightarrow (1_{R} \in {Base}_{R} \land F (1_{R}) \in J))$
32	31	biimpa	$⊢ (F Fn {Base}_{R} \land 1_{R} \in F^{-1} [J]) \to (1_{R} \in {Base}_{R} \land F (1_{R}) \in J)$
33	25 30 32	syl2anc	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to (1_{R} \in {Base}_{R} \land F (1_{R}) \in J)$
34	33	simprd	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to F (1_{R}) \in J$
35	21 34	eqeltrrd	$⊢ ((F \in (R RingHom S) \land J \in PrmIdeal (S)) \land F^{-1} [J] = {Base}_{R}) \to 1_{S} \in J$
36	18 35	mtand	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to \neg F^{-1} [J] = {Base}_{R}$
37	36	neqned	$⊢ (F \in (R RingHom S) \land J \in PrmIdeal (S)) \to F^{-1} [J] \neq {Base}_{R}$
38	37	adantll	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to F^{-1} [J] \neq {Base}_{R}$
39		simp-5l	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to S \in CRing$
40		simp-4r	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to J \in PrmIdeal (S)$
41		simp-5r	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F \in (R RingHom S)$
42	41 23	syl	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F : {Base}_{R} ⟶ {Base}_{S}$
43		simpllr	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to a \in {Base}_{R}$
44	42 43	ffvelcdmd	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F (a) \in {Base}_{S}$
45		simplr	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to b \in {Base}_{R}$
46	42 45	ffvelcdmd	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F (b) \in {Base}_{S}$
47		eqid	$⊢ \cdot_{R} = \cdot_{R}$
48	22 47 13	rhmmul	$⊢ (F \in (R RingHom S) \land a \in {Base}_{R} \land b \in {Base}_{R}) \to F (a \cdot_{R} b) = F (a) \cdot_{S} F (b)$
49	41 43 45 48	syl3anc	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F (a \cdot_{R} b) = F (a) \cdot_{S} F (b)$
50	24	ad5antlr	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F Fn {Base}_{R}$
51		simpr	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to a \cdot_{R} b \in F^{-1} [J]$
52		elpreima	$⊢ F Fn {Base}_{R} \to (a \cdot_{R} b \in F^{-1} [J] \leftrightarrow (a \cdot_{R} b \in {Base}_{R} \land F (a \cdot_{R} b) \in J))$
53	52	simplbda	$⊢ (F Fn {Base}_{R} \land a \cdot_{R} b \in F^{-1} [J]) \to F (a \cdot_{R} b) \in J$
54	50 51 53	syl2anc	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F (a \cdot_{R} b) \in J$
55	49 54	eqeltrrd	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to F (a) \cdot_{S} F (b) \in J$
56	12 13	prmidlc	$⊢ ((S \in CRing \land J \in PrmIdeal (S)) \land (F (a) \in {Base}_{S} \land F (b) \in {Base}_{S} \land F (a) \cdot_{S} F (b) \in J)) \to (F (a) \in J \lor F (b) \in J)$
57	39 40 44 46 55 56	syl23anc	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to (F (a) \in J \lor F (b) \in J)$
58	50	adantr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (a) \in J) \to F Fn {Base}_{R}$
59	43	adantr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (a) \in J) \to a \in {Base}_{R}$
60		simpr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (a) \in J) \to F (a) \in J$
61	58 59 60	elpreimad	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (a) \in J) \to a \in F^{-1} [J]$
62	61	ex	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to (F (a) \in J \to a \in F^{-1} [J])$
63	50	adantr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (b) \in J) \to F Fn {Base}_{R}$
64		simpllr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (b) \in J) \to b \in {Base}_{R}$
65		simpr	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (b) \in J) \to F (b) \in J$
66	63 64 65	elpreimad	$⊢ ((((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \land F (b) \in J) \to b \in F^{-1} [J]$
67	66	ex	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to (F (b) \in J \to b \in F^{-1} [J])$
68	62 67	orim12d	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to ((F (a) \in J \lor F (b) \in J) \to (a \in F^{-1} [J] \lor b \in F^{-1} [J]))$
69	57 68	mpd	$⊢ (((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \land a \cdot_{R} b \in F^{-1} [J]) \to (a \in F^{-1} [J] \lor b \in F^{-1} [J])$
70	69	ex	$⊢ ((((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land a \in {Base}_{R}) \land b \in {Base}_{R}) \to (a \cdot_{R} b \in F^{-1} [J] \to (a \in F^{-1} [J] \lor b \in F^{-1} [J]))$
71	70	anasss	$⊢ (((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \land (a \in {Base}_{R} \land b \in {Base}_{R})) \to (a \cdot_{R} b \in F^{-1} [J] \to (a \in F^{-1} [J] \lor b \in F^{-1} [J]))$
72	71	ralrimivva	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to \forall a \in {Base}_{R} \forall b \in {Base}_{R} (a \cdot_{R} b \in F^{-1} [J] \to (a \in F^{-1} [J] \lor b \in F^{-1} [J]))$
73	22 47	prmidl2	$⊢ ((R \in Ring \land F^{-1} [J] \in LIdeal (R)) \land (F^{-1} [J] \neq {Base}_{R} \land \forall a \in {Base}_{R} \forall b \in {Base}_{R} (a \cdot_{R} b \in F^{-1} [J] \to (a \in F^{-1} [J] \lor b \in F^{-1} [J])))) \to F^{-1} [J] \in PrmIdeal (R)$
74	3 10 38 72 73	syl22anc	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to F^{-1} [J] \in PrmIdeal (R)$
75	74 1	eleqtrrdi	$⊢ ((S \in CRing \land F \in (R RingHom S)) \land J \in PrmIdeal (S)) \to F^{-1} [J] \in P$

Metamath Proof Explorer

Theorem rhmpreimaprmidl

Proof