rprmirred

Description: In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmirred.p	$⊢ P = RPrime (R)$
	rprmirred.i	$⊢ I = Irred (R)$
	rprmirred.q	$⊢ φ \to Q \in P$
	rprmirred.r	$⊢ φ \to R \in IDomn$
Assertion	rprmirred	$⊢ φ \to Q \in I$

Proof

Step	Hyp	Ref	Expression
1		rprmirred.p	$⊢ P = RPrime (R)$
2		rprmirred.i	$⊢ I = Irred (R)$
3		rprmirred.q	$⊢ φ \to Q \in P$
4		rprmirred.r	$⊢ φ \to R \in IDomn$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 1 4 3	rprmcl	$⊢ φ \to Q \in {Base}_{R}$
7		eqid	$⊢ Unit (R) = Unit (R)$
8	1 7 4 3	rprmnunit	$⊢ φ \to \neg Q \in Unit (R)$
9	6 8	eldifd	$⊢ φ \to Q \in ({Base}_{R} ∖ Unit (R))$
10		eqid	$⊢ 0_{R} = 0_{R}$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
13	4	ad3antrrr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to R \in IDomn$
14	13	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to R \in IDomn$
15	1 10 4 3	rprmnz	$⊢ φ \to Q \neq 0_{R}$
16	15	ad4antr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to Q \neq 0_{R}$
17		simpllr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to x \in ({Base}_{R} ∖ Unit (R))$
18	17	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to x \in ({Base}_{R} ∖ Unit (R))$
19		simplr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to y \in ({Base}_{R} ∖ Unit (R))$
20	19	eldifad	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to y \in {Base}_{R}$
21	20	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to y \in {Base}_{R}$
22		simplr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to x \cdot_{R} y = Q$
23	22	eqcomd	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to Q = x \cdot_{R} y$
24		simpr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to Q ∥_{r} (R) x$
25	5 7 10 11 12 14 16 18 21 23 24	rprmirredlem	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to y \in Unit (R)$
26	19	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to y \in ({Base}_{R} ∖ Unit (R))$
27	26	eldifbd	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to \neg y \in Unit (R)$
28	25 27	pm2.21fal	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) x) \to ⊥$
29	13	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to R \in IDomn$
30	15	ad4antr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to Q \neq 0_{R}$
31	19	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to y \in ({Base}_{R} ∖ Unit (R))$
32	17	eldifad	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to x \in {Base}_{R}$
33	32	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to x \in {Base}_{R}$
34		simplr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to x \cdot_{R} y = Q$
35	29	idomcringd	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to R \in CRing$
36	20	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to y \in {Base}_{R}$
37	5 11 35 33 36	crngcomd	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to x \cdot_{R} y = y \cdot_{R} x$
38	34 37	eqtr3d	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to Q = y \cdot_{R} x$
39		simpr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to Q ∥_{r} (R) y$
40	5 7 10 11 12 29 30 31 33 38 39	rprmirredlem	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to x \in Unit (R)$
41	17	adantr	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to x \in ({Base}_{R} ∖ Unit (R))$
42	41	eldifbd	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to \neg x \in Unit (R)$
43	40 42	pm2.21fal	$⊢ ((((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \land Q ∥_{r} (R) y) \to ⊥$
44	3	ad3antrrr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to Q \in P$
45	4	idomringd	$⊢ φ \to R \in Ring$
46	5 12	dvdsrid	$⊢ (R \in Ring \land Q \in {Base}_{R}) \to Q ∥_{r} (R) Q$
47	45 6 46	syl2anc	$⊢ φ \to Q ∥_{r} (R) Q$
48	47	ad3antrrr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to Q ∥_{r} (R) Q$
49		simpr	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to x \cdot_{R} y = Q$
50	48 49	breqtrrd	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to Q ∥_{r} (R) (x \cdot_{R} y)$
51	5 1 12 11 13 44 32 20 50	rprmdvds	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to (Q ∥_{r} (R) x \lor Q ∥_{r} (R) y)$
52	28 43 51	mpjaodan	$⊢ (((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \land x \cdot_{R} y = Q) \to ⊥$
53	52	inegd	$⊢ ((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \to \neg x \cdot_{R} y = Q$
54	53	neqned	$⊢ ((φ \land x \in ({Base}_{R} ∖ Unit (R))) \land y \in ({Base}_{R} ∖ Unit (R))) \to x \cdot_{R} y \neq Q$
55	54	anasss	$⊢ (φ \land (x \in ({Base}_{R} ∖ Unit (R)) \land y \in ({Base}_{R} ∖ Unit (R)))) \to x \cdot_{R} y \neq Q$
56	55	ralrimivva	$⊢ φ \to \forall x \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y \neq Q$
57		eqid	$⊢ {Base}_{R} ∖ Unit (R) = {Base}_{R} ∖ Unit (R)$
58	5 7 2 57 11	isirred	$⊢ Q \in I \leftrightarrow (Q \in ({Base}_{R} ∖ Unit (R)) \land \forall x \in ({Base}_{R} ∖ Unit (R)) \forall y \in ({Base}_{R} ∖ Unit (R)) x \cdot_{R} y \neq Q)$
59	9 56 58	sylanbrc	$⊢ φ \to Q \in I$

Metamath Proof Explorer

Theorem rprmirred

Proof