rprmirredb

Description: In a principal ideal domain, the converse of rprmirred holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmirredb.p	$⊢ P = RPrime (R)$
	rprmirredb.i	$⊢ I = Irred (R)$
	rprmirredb.r	$⊢ φ \to R \in PID$
Assertion	rprmirredb	$⊢ φ \to I = P$

Proof

Step	Hyp	Ref	Expression
1		rprmirredb.p	$⊢ P = RPrime (R)$
2		rprmirredb.i	$⊢ I = Irred (R)$
3		rprmirredb.r	$⊢ φ \to R \in PID$
4	3	adantr	$⊢ (φ \land p \in I) \to R \in PID$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	2 5	irredcl	$⊢ p \in I \to p \in {Base}_{R}$
7	6	adantl	$⊢ (φ \land p \in I) \to p \in {Base}_{R}$
8		eqid	$⊢ Unit (R) = Unit (R)$
9	2 8	irrednu	$⊢ p \in I \to \neg p \in Unit (R)$
10	9	adantl	$⊢ (φ \land p \in I) \to \neg p \in Unit (R)$
11		df-pid	$⊢ PID = IDomn \cap LPIR$
12	3 11	eleqtrdi	$⊢ φ \to R \in (IDomn \cap LPIR)$
13	12	elin1d	$⊢ φ \to R \in IDomn$
14	13	idomringd	$⊢ φ \to R \in Ring$
15	14	adantr	$⊢ (φ \land p \in I) \to R \in Ring$
16		simpr	$⊢ (φ \land p \in I) \to p \in I$
17		eqid	$⊢ 0_{R} = 0_{R}$
18	2 17	irredn0	$⊢ (R \in Ring \land p \in I) \to p \neq 0_{R}$
19	15 16 18	syl2anc	$⊢ (φ \land p \in I) \to p \neq 0_{R}$
20		nelsn	$⊢ p \neq 0_{R} \to \neg p \in \{0_{R}\}$
21	19 20	syl	$⊢ (φ \land p \in I) \to \neg p \in \{0_{R}\}$
22		eqid	$⊢ Unit (R) \cup \{0_{R}\} = Unit (R) \cup \{0_{R}\}$
23		nelun	$⊢ Unit (R) \cup \{0_{R}\} = Unit (R) \cup \{0_{R}\} \to (\neg p \in (Unit (R) \cup \{0_{R}\}) \leftrightarrow (\neg p \in Unit (R) \land \neg p \in \{0_{R}\}))$
24	22 23	ax-mp	$⊢ \neg p \in (Unit (R) \cup \{0_{R}\}) \leftrightarrow (\neg p \in Unit (R) \land \neg p \in \{0_{R}\})$
25	10 21 24	sylanbrc	$⊢ (φ \land p \in I) \to \neg p \in (Unit (R) \cup \{0_{R}\})$
26	7 25	eldifd	$⊢ (φ \land p \in I) \to p \in ({Base}_{R} ∖ (Unit (R) \cup \{0_{R}\}))$
27		eqid	$⊢ RSpan (R) = RSpan (R)$
28		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
29	15	ad3antrrr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to R \in Ring$
30	7	ad3antrrr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to p \in {Base}_{R}$
31	5 27 28 29 30	ellpi	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to (x \in RSpan (R) (\{p\}) \leftrightarrow p ∥_{r} (R) x)$
32	31	biimpa	$⊢ (((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \land x \in RSpan (R) (\{p\})) \to p ∥_{r} (R) x$
33	5 27 28 29 30	ellpi	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to (y \in RSpan (R) (\{p\}) \leftrightarrow p ∥_{r} (R) y)$
34	33	biimpa	$⊢ (((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \land y \in RSpan (R) (\{p\})) \to p ∥_{r} (R) y$
35	13	idomcringd	$⊢ φ \to R \in CRing$
36	35	ad4antr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to R \in CRing$
37	2	eleq2i	$⊢ p \in I \leftrightarrow p \in Irred (R)$
38	37	bilani	$⊢ (φ \land p \in I) \to p \in Irred (R)$
39		eqid	$⊢ RSpan (R) (\{p\}) = RSpan (R) (\{p\})$
40	7	snssd	$⊢ (φ \land p \in I) \to \{p\} \subseteq {Base}_{R}$
41		eqid	$⊢ LIdeal (R) = LIdeal (R)$
42	27 5 41	rspcl	$⊢ (R \in Ring \land \{p\} \subseteq {Base}_{R}) \to RSpan (R) (\{p\}) \in LIdeal (R)$
43	15 40 42	syl2anc	$⊢ (φ \land p \in I) \to RSpan (R) (\{p\}) \in LIdeal (R)$
44	5 27 17 39 4 7 19 43	mxidlirred	$⊢ (φ \land p \in I) \to (RSpan (R) (\{p\}) \in MaxIdeal (R) \leftrightarrow p \in Irred (R))$
45	38 44	mpbird	$⊢ (φ \land p \in I) \to RSpan (R) (\{p\}) \in MaxIdeal (R)$
46	45	ad3antrrr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to RSpan (R) (\{p\}) \in MaxIdeal (R)$
47		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
48	47	mxidlprm	$⊢ (R \in CRing \land RSpan (R) (\{p\}) \in MaxIdeal (R)) \to RSpan (R) (\{p\}) \in PrmIdeal (R)$
49	36 46 48	syl2anc	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to RSpan (R) (\{p\}) \in PrmIdeal (R)$
50		simpllr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to x \in {Base}_{R}$
51		simplr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to y \in {Base}_{R}$
52		simpr	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to p ∥_{r} (R) (x \cdot_{R} y)$
53	5 27 28 29 30	ellpi	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to (x \cdot_{R} y \in RSpan (R) (\{p\}) \leftrightarrow p ∥_{r} (R) (x \cdot_{R} y))$
54	52 53	mpbird	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to x \cdot_{R} y \in RSpan (R) (\{p\})$
55		eqid	$⊢ \cdot_{R} = \cdot_{R}$
56	5 55	prmidlc	$⊢ ((R \in CRing \land RSpan (R) (\{p\}) \in PrmIdeal (R)) \land (x \in {Base}_{R} \land y \in {Base}_{R} \land x \cdot_{R} y \in RSpan (R) (\{p\}))) \to (x \in RSpan (R) (\{p\}) \lor y \in RSpan (R) (\{p\}))$
57	36 49 50 51 54 56	syl23anc	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to (x \in RSpan (R) (\{p\}) \lor y \in RSpan (R) (\{p\}))$
58	32 34 57	orim12da	$⊢ ((((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \land p ∥_{r} (R) (x \cdot_{R} y)) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y)$
59	58	ex	$⊢ (((φ \land p \in I) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to (p ∥_{r} (R) (x \cdot_{R} y) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y))$
60	59	anasss	$⊢ ((φ \land p \in I) \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to (p ∥_{r} (R) (x \cdot_{R} y) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y))$
61	60	ralrimivva	$⊢ (φ \land p \in I) \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} (p ∥_{r} (R) (x \cdot_{R} y) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y))$
62	5 8 17 28 55	isrprm	$⊢ R \in PID \to (p \in RPrime (R) \leftrightarrow (p \in ({Base}_{R} ∖ (Unit (R) \cup \{0_{R}\})) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (p ∥_{r} (R) (x \cdot_{R} y) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y))))$
63	62	biimpar	$⊢ (R \in PID \land (p \in ({Base}_{R} ∖ (Unit (R) \cup \{0_{R}\})) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} (p ∥_{r} (R) (x \cdot_{R} y) \to (p ∥_{r} (R) x \lor p ∥_{r} (R) y)))) \to p \in RPrime (R)$
64	4 26 61 63	syl12anc	$⊢ (φ \land p \in I) \to p \in RPrime (R)$
65	64 1	eleqtrrdi	$⊢ (φ \land p \in I) \to p \in P$
66		simpr	$⊢ (φ \land p \in P) \to p \in P$
67	13	adantr	$⊢ (φ \land p \in P) \to R \in IDomn$
68	1 2 66 67	rprmirred	$⊢ (φ \land p \in P) \to p \in I$
69	65 68	impbida	$⊢ φ \to (p \in I \leftrightarrow p \in P)$
70	69	eqrdv	$⊢ φ \to I = P$

Metamath Proof Explorer

Theorem rprmirredb

Proof