rprmasso2

Description: In an integral domain, if a prime element divides another, they are associates. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmasso.b	$⊢ B = {Base}_{R}$
	rprmasso.p	$⊢ P = RPrime (R)$
	rprmasso.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	rprmasso.r	$⊢ φ \to R \in IDomn$
	rprmasso.x	$⊢ φ \to X \in P$
	rprmasso.1	$⊢ φ \to X \underset{˙}{∥} Y$
	rprmasso2.y	$⊢ φ \to Y \in P$
Assertion	rprmasso2	$⊢ φ \to Y \underset{˙}{∥} X$

Proof

Step	Hyp	Ref	Expression
1		rprmasso.b	$⊢ B = {Base}_{R}$
2		rprmasso.p	$⊢ P = RPrime (R)$
3		rprmasso.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
4		rprmasso.r	$⊢ φ \to R \in IDomn$
5		rprmasso.x	$⊢ φ \to X \in P$
6		rprmasso.1	$⊢ φ \to X \underset{˙}{∥} Y$
7		rprmasso2.y	$⊢ φ \to Y \in P$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9	4	ad2antrr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to R \in IDomn$
10	7	ad2antrr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to Y \in P$
11		simplr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to t \in B$
12	1 2 4 5	rprmcl	$⊢ φ \to X \in B$
13	12	ad2antrr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to X \in B$
14	4	idomringd	$⊢ φ \to R \in Ring$
15	1 2 4 7	rprmcl	$⊢ φ \to Y \in B$
16	1 3	dvdsrid	$⊢ (R \in Ring \land Y \in B) \to Y \underset{˙}{∥} Y$
17	14 15 16	syl2anc	$⊢ φ \to Y \underset{˙}{∥} Y$
18	17	ad2antrr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to Y \underset{˙}{∥} Y$
19		simpr	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to t \cdot_{R} X = Y$
20	18 19	breqtrrd	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to Y \underset{˙}{∥} (t \cdot_{R} X)$
21	1 2 3 8 9 10 11 13 20	rprmdvds	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to (Y \underset{˙}{∥} t \lor Y \underset{˙}{∥} X)$
22	12	ad3antrrr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to X \in B$
23		eqid	$⊢ 0_{R} = 0_{R}$
24	11	ad3antrrr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \in B$
25		simpr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to t = 0_{R}$
26	25	oveq1d	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to t \cdot_{R} X = 0_{R} \cdot_{R} X$
27		simplr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to t \cdot_{R} X = Y$
28	1 8 23 14 12	ringlzd	$⊢ φ \to 0_{R} \cdot_{R} X = 0_{R}$
29	28	ad3antrrr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to 0_{R} \cdot_{R} X = 0_{R}$
30	26 27 29	3eqtr3d	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to Y = 0_{R}$
31	2 23 4 7	rprmnz	$⊢ φ \to Y \neq 0_{R}$
32	31	ad3antrrr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to Y \neq 0_{R}$
33	32	neneqd	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land t = 0_{R}) \to \neg Y = 0_{R}$
34	30 33	pm2.65da	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to \neg t = 0_{R}$
35	34	neqned	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to t \neq 0_{R}$
36	35	ad3antrrr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \neq 0_{R}$
37	24 36	eldifsnd	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \in (B ∖ \{0_{R}\})$
38	14	ad5antr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to R \in Ring$
39		simplr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \in B$
40	13	ad3antrrr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to X \in B$
41	1 8 38 39 40	ringcld	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \cdot_{R} X \in B$
42		eqid	$⊢ 1_{R} = 1_{R}$
43	1 42	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
44	14 43	syl	$⊢ φ \to 1_{R} \in B$
45	44	ad5antr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to 1_{R} \in B$
46	4	idomdomd	$⊢ φ \to R \in Domn$
47	46	ad5antr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to R \in Domn$
48	19	ad3antrrr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \cdot_{R} X = Y$
49	48	oveq2d	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \cdot_{R} (t \cdot_{R} X) = u \cdot_{R} Y$
50		simpr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \cdot_{R} Y = t$
51	49 50	eqtrd	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \cdot_{R} (t \cdot_{R} X) = t$
52	4	idomcringd	$⊢ φ \to R \in CRing$
53	52	ad5antr	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to R \in CRing$
54	1 8 53 24 39 40	crng12d	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \cdot_{R} (u \cdot_{R} X) = u \cdot_{R} (t \cdot_{R} X)$
55	1 8 42 38 24	ringridmd	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \cdot_{R} 1_{R} = t$
56	51 54 55	3eqtr4d	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to t \cdot_{R} (u \cdot_{R} X) = t \cdot_{R} 1_{R}$
57	1 23 8 37 41 45 47 56	domnlcan	$⊢ (((((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \land u \in B) \land u \cdot_{R} Y = t) \to u \cdot_{R} X = 1_{R}$
58	15	ad3antrrr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to Y \in B$
59		simpr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to Y \underset{˙}{∥} t$
60	1 3 8	dvdsr2	$⊢ Y \in B \to (Y \underset{˙}{∥} t \leftrightarrow \exists u \in B u \cdot_{R} Y = t)$
61	60	biimpa	$⊢ (Y \in B \land Y \underset{˙}{∥} t) \to \exists u \in B u \cdot_{R} Y = t$
62	58 59 61	syl2anc	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to \exists u \in B u \cdot_{R} Y = t$
63	57 62	reximddv3	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to \exists u \in B u \cdot_{R} X = 1_{R}$
64	1 3 8	dvdsr2	$⊢ X \in B \to (X \underset{˙}{∥} 1_{R} \leftrightarrow \exists u \in B u \cdot_{R} X = 1_{R})$
65	64	biimpar	$⊢ (X \in B \land \exists u \in B u \cdot_{R} X = 1_{R}) \to X \underset{˙}{∥} 1_{R}$
66	22 63 65	syl2anc	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to X \underset{˙}{∥} 1_{R}$
67	42 3 2 52 5	rprmndvdsr1	$⊢ φ \to \neg X \underset{˙}{∥} 1_{R}$
68	67	ad3antrrr	$⊢ (((φ \land t \in B) \land t \cdot_{R} X = Y) \land Y \underset{˙}{∥} t) \to \neg X \underset{˙}{∥} 1_{R}$
69	66 68	pm2.65da	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to \neg Y \underset{˙}{∥} t$
70	21 69	orcnd	$⊢ ((φ \land t \in B) \land t \cdot_{R} X = Y) \to Y \underset{˙}{∥} X$
71	1 3 8	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists t \in B t \cdot_{R} X = Y)$
72	6 71	sylib	$⊢ φ \to (X \in B \land \exists t \in B t \cdot_{R} X = Y)$
73	72	simprd	$⊢ φ \to \exists t \in B t \cdot_{R} X = Y$
74	70 73	r19.29a	$⊢ φ \to Y \underset{˙}{∥} X$

Metamath Proof Explorer

Theorem rprmasso2

Proof