Metamath Proof Explorer

Theorem ufdprmidl

Description: In a unique factorization domain R , a nonzero prime ideal J contains a prime element p . (Contributed by Thierry Arnoux, 3-Jun-2025)

		Ref	Expression
	Hypotheses	isufd.i	$⊢ I = PrmIdeal (R)$
		isufd.3	$⊢ P = RPrime (R)$
		isufd.0	$⊢ \underset{˙}{0} = 0_{R}$
		ufdprmidl.2	$⊢ φ \to R \in UFD$
		ufdprmidl.3	$⊢ φ \to J \in I$
		ufdprmidl.4	$⊢ φ \to J \neq \{\underset{˙}{0}\}$
	Assertion	ufdprmidl	$⊢ φ \to \exists p \in P p \in J$

Proof

Step	Hyp	Ref	Expression
1		isufd.i	$⊢ I = PrmIdeal (R)$
2		isufd.3	$⊢ P = RPrime (R)$
3		isufd.0	$⊢ \underset{˙}{0} = 0_{R}$
4		ufdprmidl.2	$⊢ φ \to R \in UFD$
5		ufdprmidl.3	$⊢ φ \to J \in I$
6		ufdprmidl.4	$⊢ φ \to J \neq \{\underset{˙}{0}\}$
7		ineq1	$⊢ j = J \to j \cap P = J \cap P$
8	7	neeq1d	$⊢ j = J \to (j \cap P \neq \emptyset \leftrightarrow J \cap P \neq \emptyset)$
9	8	adantl	$⊢ (φ \land j = J) \to (j \cap P \neq \emptyset \leftrightarrow J \cap P \neq \emptyset)$
10		incom	$⊢ P \cap J = J \cap P$
11	10	neeq1i	$⊢ P \cap J \neq \emptyset \leftrightarrow J \cap P \neq \emptyset$
12		inn0	$⊢ P \cap J \neq \emptyset \leftrightarrow \exists p \in P p \in J$
13	11 12	bitr3i	$⊢ J \cap P \neq \emptyset \leftrightarrow \exists p \in P p \in J$
14	9 13	bitrdi	$⊢ (φ \land j = J) \to (j \cap P \neq \emptyset \leftrightarrow \exists p \in P p \in J)$
15	5 6	eldifsnd	$⊢ φ \to J \in (I ∖ \{\{\underset{˙}{0}\}\})$
16	1 2 3	isufd	$⊢ R \in UFD \leftrightarrow (R \in IDomn \land \forall j \in (I ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset)$
17	16	simprbi	$⊢ R \in UFD \to \forall j \in (I ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset$
18	4 17	syl	$⊢ φ \to \forall j \in (I ∖ \{\{\underset{˙}{0}\}\}) j \cap P \neq \emptyset$
19	14 15 18	rspcdv2	$⊢ φ \to \exists p \in P p \in J$