Metamath Proof Explorer

Theorem rprmndvdsru

Description: A ring prime element does not divide any ring unit. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses rprmndvdsru.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
rprmndvdsru.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmndvdsru.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmndvdsru.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rprmndvdsru.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
rprmndvdsru.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
Assertion rprmndvdsru ( 𝜑 → ¬ 𝑄 ∥ 𝑇 )

Proof

Step Hyp Ref Expression
1 rprmndvdsru.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 rprmndvdsru.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 rprmndvdsru.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 rprmndvdsru.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 rprmndvdsru.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
6 rprmndvdsru.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 7 3 2 4 5 rprmndvdsr1 ⊢ ( 𝜑 → ¬ 𝑄 ∥ ( 1r ‘ 𝑅 ) )
9 4 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 1 7 3 crngunit ⊢ ( 𝑅 ∈ CRing → ( 𝑇 ∈ 𝑈 ↔ 𝑇 ∥ ( 1r ‘ 𝑅 ) ) )
11 10 biimpa ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑇 ∈ 𝑈 ) → 𝑇 ∥ ( 1r ‘ 𝑅 ) )
12 4 6 11 syl2anc ⊢ ( 𝜑 → 𝑇 ∥ ( 1r ‘ 𝑅 ) )
13 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 13 3 dvdsrtr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∥ 𝑇 ∧ 𝑇 ∥ ( 1r ‘ 𝑅 ) ) → 𝑄 ∥ ( 1r ‘ 𝑅 ) )
15 14 3expa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑄 ∥ 𝑇 ) ∧ 𝑇 ∥ ( 1r ‘ 𝑅 ) ) → 𝑄 ∥ ( 1r ‘ 𝑅 ) )
16 15 an32s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ∥ ( 1r ‘ 𝑅 ) ) ∧ 𝑄 ∥ 𝑇 ) → 𝑄 ∥ ( 1r ‘ 𝑅 ) )
17 16 ex ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ∥ ( 1r ‘ 𝑅 ) ) → ( 𝑄 ∥ 𝑇 → 𝑄 ∥ ( 1r ‘ 𝑅 ) ) )
18 9 12 17 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∥ 𝑇 → 𝑄 ∥ ( 1r ‘ 𝑅 ) ) )
19 8 18 mtod ⊢ ( 𝜑 → ¬ 𝑄 ∥ 𝑇 )