rsprprmprmidlb

Description: In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rsprprmprmidlb.0	$⊢ \underset{˙}{0} = 0_{R}$
	rsprprmprmidlb.b	$⊢ B = {Base}_{R}$
	rsprprmprmidlb.p	$⊢ P = RPrime (R)$
	rsprprmprmidlb.k	$⊢ K = RSpan (R)$
	rsprprmprmidlb.r	$⊢ φ \to R \in IDomn$
	rsprprmprmidlb.x	$⊢ φ \to X \in B$
	rsprprmprmidlb.1	$⊢ φ \to X \neq \underset{˙}{0}$
Assertion	rsprprmprmidlb	$⊢ φ \to (X \in P \leftrightarrow K (\{X\}) \in PrmIdeal (R))$

Proof

Step	Hyp	Ref	Expression
1		rsprprmprmidlb.0	$⊢ \underset{˙}{0} = 0_{R}$
2		rsprprmprmidlb.b	$⊢ B = {Base}_{R}$
3		rsprprmprmidlb.p	$⊢ P = RPrime (R)$
4		rsprprmprmidlb.k	$⊢ K = RSpan (R)$
5		rsprprmprmidlb.r	$⊢ φ \to R \in IDomn$
6		rsprprmprmidlb.x	$⊢ φ \to X \in B$
7		rsprprmprmidlb.1	$⊢ φ \to X \neq \underset{˙}{0}$
8	5	idomcringd	$⊢ φ \to R \in CRing$
9	8	adantr	$⊢ (φ \land X \in P) \to R \in CRing$
10	3	a1i	$⊢ φ \to P = RPrime (R)$
11	10	eleq2d	$⊢ φ \to (X \in P \leftrightarrow X \in RPrime (R))$
12	11	biimpa	$⊢ (φ \land X \in P) \to X \in RPrime (R)$
13	4 9 12	rsprprmprmidl	$⊢ (φ \land X \in P) \to K (\{X\}) \in PrmIdeal (R)$
14	5	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to R \in IDomn$
15	6	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in B$
16		eqid	$⊢ Unit (R) = Unit (R)$
17		eqid	$⊢ K (\{X\}) = K (\{X\})$
18	16 4 17 2 15 14	unitpidl1	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to (K (\{X\}) = B \leftrightarrow X \in Unit (R))$
19	18	biimpar	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to K (\{X\}) = B$
20	14	idomringd	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to R \in Ring$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22	2 21	prmidlnr	$⊢ (R \in Ring \land K (\{X\}) \in PrmIdeal (R)) \to K (\{X\}) \neq B$
23	20 22	sylancom	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to K (\{X\}) \neq B$
24	23	adantr	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to K (\{X\}) \neq B$
25	24	neneqd	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to \neg K (\{X\}) = B$
26	19 25	pm2.65da	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in Unit (R)$
27		nelsn	$⊢ X \neq \underset{˙}{0} \to \neg X \in \{\underset{˙}{0}\}$
28	7 27	syl	$⊢ φ \to \neg X \in \{\underset{˙}{0}\}$
29	28	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in \{\underset{˙}{0}\}$
30		eqid	$⊢ Unit (R) \cup \{\underset{˙}{0}\} = Unit (R) \cup \{\underset{˙}{0}\}$
31		nelun	$⊢ Unit (R) \cup \{\underset{˙}{0}\} = Unit (R) \cup \{\underset{˙}{0}\} \to (\neg X \in (Unit (R) \cup \{\underset{˙}{0}\}) \leftrightarrow (\neg X \in Unit (R) \land \neg X \in \{\underset{˙}{0}\}))$
32	30 31	ax-mp	$⊢ \neg X \in (Unit (R) \cup \{\underset{˙}{0}\}) \leftrightarrow (\neg X \in Unit (R) \land \neg X \in \{\underset{˙}{0}\})$
33	26 29 32	sylanbrc	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in (Unit (R) \cup \{\underset{˙}{0}\})$
34	15 33	eldifd	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in (B ∖ (Unit (R) \cup \{\underset{˙}{0}\}))$
35		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
36	20	ad3antrrr	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to R \in Ring$
37	6	ad4antr	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to X \in B$
38	2 4 35 36 37	ellpi	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to (x \in K (\{X\}) \leftrightarrow X ∥_{r} (R) x)$
39	38	biimpa	$⊢ (((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \land x \in K (\{X\})) \to X ∥_{r} (R) x$
40	2 4 35 36 37	ellpi	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to (y \in K (\{X\}) \leftrightarrow X ∥_{r} (R) y)$
41	40	biimpa	$⊢ (((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \land y \in K (\{X\})) \to X ∥_{r} (R) y$
42	8	ad4antr	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to R \in CRing$
43		simp-4r	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to K (\{X\}) \in PrmIdeal (R)$
44		simpllr	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to x \in B$
45		simplr	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to y \in B$
46	20	ad2antrr	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to R \in Ring$
47	6	ad3antrrr	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to X \in B$
48	2 4 35 46 47	ellpi	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to (x \cdot_{R} y \in K (\{X\}) \leftrightarrow X ∥_{r} (R) (x \cdot_{R} y))$
49	48	biimpar	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to x \cdot_{R} y \in K (\{X\})$
50	2 21	prmidlc	$⊢ ((R \in CRing \land K (\{X\}) \in PrmIdeal (R)) \land (x \in B \land y \in B \land x \cdot_{R} y \in K (\{X\}))) \to (x \in K (\{X\}) \lor y \in K (\{X\}))$
51	42 43 44 45 49 50	syl23anc	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to (x \in K (\{X\}) \lor y \in K (\{X\}))$
52	39 41 51	orim12da	$⊢ ((((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \land X ∥_{r} (R) (x \cdot_{R} y)) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y)$
53	52	ex	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to (X ∥_{r} (R) (x \cdot_{R} y) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y))$
54	53	anasss	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land (x \in B \land y \in B)) \to (X ∥_{r} (R) (x \cdot_{R} y) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y))$
55	54	ralrimivva	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \forall x \in B \forall y \in B (X ∥_{r} (R) (x \cdot_{R} y) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y))$
56	2 16 1 35 21	isrprm	$⊢ R \in IDomn \to (X \in RPrime (R) \leftrightarrow (X \in (B ∖ (Unit (R) \cup \{\underset{˙}{0}\})) \land \forall x \in B \forall y \in B (X ∥_{r} (R) (x \cdot_{R} y) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y))))$
57	56	biimpar	$⊢ (R \in IDomn \land (X \in (B ∖ (Unit (R) \cup \{\underset{˙}{0}\})) \land \forall x \in B \forall y \in B (X ∥_{r} (R) (x \cdot_{R} y) \to (X ∥_{r} (R) x \lor X ∥_{r} (R) y)))) \to X \in RPrime (R)$
58	14 34 55 57	syl12anc	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in RPrime (R)$
59	58 3	eleqtrrdi	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in P$
60	13 59	impbida	$⊢ φ \to (X \in P \leftrightarrow K (\{X\}) \in PrmIdeal (R))$

Metamath Proof Explorer

Theorem rsprprmprmidlb

Proof