Metamath Proof Explorer

Theorem unitmulrprm

Description: A ring unit multiplied by a ring prime is a ring prime. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses unitmulrprm.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
unitmulrprm.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitmulrprm.t ⊢ · = ( .r ‘ 𝑅 )
unitmulrprm.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
unitmulrprm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
unitmulrprm.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
Assertion unitmulrprm ( 𝜑 → ( 𝐼 · 𝑄 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 unitmulrprm.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
2 unitmulrprm.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 unitmulrprm.t ⊢ · = ( .r ‘ 𝑅 )
4 unitmulrprm.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 unitmulrprm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
6 unitmulrprm.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
9 7 1 4 6 rprmcl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑅 ) )
10 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 · 𝑄 ) = ( 𝐼 · 𝑄 ) )
11 10 eqeq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 · 𝑄 ) = ( 𝐼 · 𝑄 ) ↔ ( 𝐼 · 𝑄 ) = ( 𝐼 · 𝑄 ) ) )
12 7 2 unitcl ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ ( Base ‘ 𝑅 ) )
13 5 12 syl ⊢ ( 𝜑 → 𝐼 ∈ ( Base ‘ 𝑅 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝐼 · 𝑄 ) = ( 𝐼 · 𝑄 ) )
15 11 13 14 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 · 𝑄 ) = ( 𝐼 · 𝑄 ) )
16 7 8 3 dvdsr ⊢ ( 𝑄 ( ∥r ‘ 𝑅 ) ( 𝐼 · 𝑄 ) ↔ ( 𝑄 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 · 𝑄 ) = ( 𝐼 · 𝑄 ) ) )
17 9 15 16 sylanbrc ⊢ ( 𝜑 → 𝑄 ( ∥r ‘ 𝑅 ) ( 𝐼 · 𝑄 ) )
18 4 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
19 7 3 18 13 9 ringcld ⊢ ( 𝜑 → ( 𝐼 · 𝑄 ) ∈ ( Base ‘ 𝑅 ) )
20 oveq1 ⊢ ( 𝑖 = ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) → ( 𝑖 · ( 𝐼 · 𝑄 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · ( 𝐼 · 𝑄 ) ) )
21 20 eqeq1d ⊢ ( 𝑖 = ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) → ( ( 𝑖 · ( 𝐼 · 𝑄 ) ) = 𝑄 ↔ ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · ( 𝐼 · 𝑄 ) ) = 𝑄 ) )
22 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
23 2 22 7 ringinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
24 18 5 23 syl2anc ⊢ ( 𝜑 → ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) ∈ ( Base ‘ 𝑅 ) )
25 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26 2 22 3 25 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · 𝐼 ) = ( 1r ‘ 𝑅 ) )
27 18 5 26 syl2anc ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · 𝐼 ) = ( 1r ‘ 𝑅 ) )
28 27 oveq1d ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · 𝐼 ) · 𝑄 ) = ( ( 1r ‘ 𝑅 ) · 𝑄 ) )
29 7 3 18 24 13 9 ringassd ⊢ ( 𝜑 → ( ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · 𝐼 ) · 𝑄 ) = ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · ( 𝐼 · 𝑄 ) ) )
30 7 3 25 18 9 ringlidmd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) · 𝑄 ) = 𝑄 )
31 28 29 30 3eqtr3d ⊢ ( 𝜑 → ( ( ( invr ‘ 𝑅 ) ‘ 𝐼 ) · ( 𝐼 · 𝑄 ) ) = 𝑄 )
32 21 24 31 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 · ( 𝐼 · 𝑄 ) ) = 𝑄 )
33 7 8 3 dvdsr ⊢ ( ( 𝐼 · 𝑄 ) ( ∥r ‘ 𝑅 ) 𝑄 ↔ ( ( 𝐼 · 𝑄 ) ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 · ( 𝐼 · 𝑄 ) ) = 𝑄 ) )
34 19 32 33 sylanbrc ⊢ ( 𝜑 → ( 𝐼 · 𝑄 ) ( ∥r ‘ 𝑅 ) 𝑄 )
35 7 1 8 4 6 17 34 rprmasso ⊢ ( 𝜑 → ( 𝐼 · 𝑄 ) ∈ 𝑃 )