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	biimpi	$⊢ p \in I \to p \in Irred (R)$
39	38	adantl	$⊢ (φ \land p \in I) \to p \in Irred (R)$
40		eqid	$⊢ RSpan (R) (\{p\}) = RSpan (R) (\{p\})$
41	7	snssd	$⊢ (φ \land p \in I) \to \{p\} \subseteq {Base}_{R}$
42		eqid	$⊢ LIdeal (R) = LIdeal (R)$
43	27 5 42	rspcl	$⊢ (R \in Ring \land \{p\} \subseteq {Base}_{R}) \to RSpan (R) (\{p\}) \in LIdeal (R)$
44	15 41 43	syl2anc	$⊢ (φ \land p \in I) \to RSpan (R) (\{p\}) \in LIdeal (R)$
45	5 27 17 40 4 7 19 44	mxidlirred	Could not format ( ( ph /\ p e. I ) -> ( ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) <-> p e. ( Irred ` R ) ) ) : No typesetting found for \|- ( ( ph /\ p e. I ) -> ( ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) <-> p e. ( Irred ` R ) ) ) with typecode \|-
46	39 45	mpbird	Could not format ( ( ph /\ p e. I ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ph /\ p e. I ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) with typecode \|-
47	46	ad3antrrr	Could not format ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( \|\|r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( \|\|r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) with typecode \|-
48		eqid	$⊢ LSSum ({mulGrp}_{R}) = LSSum ({mulGrp}_{R})$
49	48	mxidlprm	Could not format ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( MaxIdeal ` R ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) with typecode \|-
50	36 47 49	syl2anc	Could not format ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( \|\|r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( ( ph /\ p e. I ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ p ( \|\|r ` R ) ( x ( .r ` R ) y ) ) -> ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) with typecode \|-
51		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}$
52		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}$
53		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)$
54	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))$
55	53 54	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\})$
56		eqid	$⊢ \cdot_{R} = \cdot_{R}$
57	5 56	prmidlc	Could not format ( ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ ( x ( .r ` R ) y ) e. ( ( RSpan ` R ) ` { p } ) ) ) -> ( x e. ( ( RSpan ` R ) ` { p } ) \/ y e. ( ( RSpan ` R ) ` { p } ) ) ) : No typesetting found for \|- ( ( ( R e. CRing /\ ( ( RSpan ` R ) ` { p } ) e. ( PrmIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ ( x ( .r ` R ) y ) e. ( ( RSpan ` R ) ` { p } ) ) ) -> ( x e. ( ( RSpan ` R ) ` { p } ) \/ y e. ( ( RSpan ` R ) ` { p } ) ) ) with typecode \|-
58	36 50 51 52 55 57	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\}))$
59	32 34 58	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)$
60	59	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))$
61	60	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))$
62	61	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))$
63	5 8 17 28 56	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))))$
64	63	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)$
65	4 26 62 64	syl12anc	$⊢ (φ \land p \in I) \to p \in RPrime (R)$
66	65 1	eleqtrrdi	$⊢ (φ \land p \in I) \to p \in P$
67		simpr	$⊢ (φ \land p \in P) \to p \in P$
68	13	adantr	$⊢ (φ \land p \in P) \to R \in IDomn$
69	1 2 67 68	rprmirred	$⊢ (φ \land p \in P) \to p \in I$
70	66 69	impbida	$⊢ φ \to (p \in I \leftrightarrow p \in P)$
71	70	eqrdv	$⊢ φ \to I = P$

Metamath Proof Explorer

Theorem rprmirredb

Proof