rsprprmprmidlb

Description: 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 CRing$
	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 CRing$
6		rsprprmprmidlb.x	$⊢ φ \to X \in B$
7		rsprprmprmidlb.1	$⊢ φ \to X \neq \underset{˙}{0}$
8	5	adantr	$⊢ (φ \land X \in P) \to R \in CRing$
9	3	a1i	$⊢ φ \to P = RPrime (R)$
10	9	eleq2d	$⊢ φ \to (X \in P \leftrightarrow X \in RPrime (R))$
11	10	biimpa	$⊢ (φ \land X \in P) \to X \in RPrime (R)$
12	4 8 11	rsprprmprmidl	$⊢ (φ \land X \in P) \to K (\{X\}) \in PrmIdeal (R)$
13	5	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to R \in CRing$
14	6	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in B$
15		eqid	$⊢ Unit (R) = Unit (R)$
16		eqid	$⊢ K (\{X\}) = K (\{X\})$
17	15 4 16 2 14 13	unitpidl1	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to (K (\{X\}) = B \leftrightarrow X \in Unit (R))$
18	17	biimpar	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to K (\{X\}) = B$
19	13	crngringd	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to R \in Ring$
20		eqid	$⊢ \cdot_{R} = \cdot_{R}$
21	2 20	prmidlnr	$⊢ (R \in Ring \land K (\{X\}) \in PrmIdeal (R)) \to K (\{X\}) \neq B$
22	19 21	sylancom	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to K (\{X\}) \neq B$
23	22	adantr	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to K (\{X\}) \neq B$
24	23	neneqd	$⊢ ((φ \land K (\{X\}) \in PrmIdeal (R)) \land X \in Unit (R)) \to \neg K (\{X\}) = B$
25	18 24	pm2.65da	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in Unit (R)$
26		nelsn	$⊢ X \neq \underset{˙}{0} \to \neg X \in \{\underset{˙}{0}\}$
27	7 26	syl	$⊢ φ \to \neg X \in \{\underset{˙}{0}\}$
28	27	adantr	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in \{\underset{˙}{0}\}$
29		eqid	$⊢ Unit (R) \cup \{\underset{˙}{0}\} = Unit (R) \cup \{\underset{˙}{0}\}$
30		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}\}))$
31	29 30	ax-mp	$⊢ \neg X \in (Unit (R) \cup \{\underset{˙}{0}\}) \leftrightarrow (\neg X \in Unit (R) \land \neg X \in \{\underset{˙}{0}\})$
32	25 28 31	sylanbrc	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to \neg X \in (Unit (R) \cup \{\underset{˙}{0}\})$
33	14 32	eldifd	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in (B ∖ (Unit (R) \cup \{\underset{˙}{0}\}))$
34		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
35	19	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$
36	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$
37	2 4 34 35 36	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)$
38	37	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$
39	2 4 34 35 36	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)$
40	39	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$
41	5	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$
42		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)$
43		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$
44		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$
45	19	ad2antrr	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to R \in Ring$
46	6	ad3antrrr	$⊢ (((φ \land K (\{X\}) \in PrmIdeal (R)) \land x \in B) \land y \in B) \to X \in B$
47	2 4 34 45 46	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))$
48	47	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\})$
49	2 20	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\}))$
50	41 42 43 44 48 49	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\}))$
51	38 40 50	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)$
52	51	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))$
53	52	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))$
54	53	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))$
55	2 15 1 34 20	isrprm	$⊢ R \in CRing \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))))$
56	55	biimpar	$⊢ (R \in CRing \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)$
57	13 33 54 56	syl12anc	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in RPrime (R)$
58	57 3	eleqtrrdi	$⊢ (φ \land K (\{X\}) \in PrmIdeal (R)) \to X \in P$
59	12 58	impbida	$⊢ φ \to (X \in P \leftrightarrow K (\{X\}) \in PrmIdeal (R))$

Metamath Proof Explorer

Theorem rsprprmprmidlb

Proof