Metamath Proof Explorer

Theorem rprmasso3

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

Ref Expression
Hypotheses rprmasso.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmasso.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmasso.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
rprmasso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
rprmasso.1 ⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
rprmasso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
rprmasso3.1 ⊢ · = ( .r ‘ 𝑅 )
rprmasso3.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion rprmasso3 ( 𝜑 → ∃ 𝑡 ∈ 𝑈 ( 𝑡 · 𝑋 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 rprmasso.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmasso.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 rprmasso.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 rprmasso.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 rprmasso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 rprmasso.1 ⊢ ( 𝜑 → 𝑋 ∥ 𝑌 )
7 rprmasso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
8 rprmasso3.1 ⊢ · = ( .r ‘ 𝑅 )
9 rprmasso3.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
10 1 2 3 4 5 6 7 rprmasso2 ⊢ ( 𝜑 → 𝑌 ∥ 𝑋 )
11 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
12 1 2 4 5 rprmcl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13 1 2 4 7 rprmcl ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
14 1 11 3 12 13 9 8 4 dvdsruasso ⊢ ( 𝜑 → ( ( 𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋 ) ↔ ∃ 𝑡 ∈ 𝑈 ( 𝑡 · 𝑋 ) = 𝑌 ) )
15 6 10 14 mpbi2and ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝑈 ( 𝑡 · 𝑋 ) = 𝑌 )