Metamath Proof Explorer

Theorem rprmdvds

Description: If a ring prime Q divides a product X .x. Y , then it divides either X or Y . (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmdvds.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmdvds.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmdvds.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
rprmdvds.t ⊢ · = ( .r ‘ 𝑅 )
rprmdvds.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
rprmdvds.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
rprmdvds.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rprmdvds.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
rprmdvds.1 ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑋 · 𝑌 ) )
Assertion rprmdvds ( 𝜑 → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 rprmdvds.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmdvds.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3 rprmdvds.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 rprmdvds.t ⊢ · = ( .r ‘ 𝑅 )
5 rprmdvds.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6 rprmdvds.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
7 rprmdvds.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 rprmdvds.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 rprmdvds.1 ⊢ ( 𝜑 → 𝑄 ∥ ( 𝑋 · 𝑌 ) )
10 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑦 ) )
11 10 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑄 ∥ ( 𝑥 · 𝑦 ) ↔ 𝑄 ∥ ( 𝑋 · 𝑦 ) ) )
12 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑄 ∥ 𝑥 ↔ 𝑄 ∥ 𝑋 ) )
13 12 orbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑄 ∥ 𝑥 ∨ 𝑄 ∥ 𝑦 ) ↔ ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑦 ) ) )
14 11 13 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑄 ∥ ( 𝑥 · 𝑦 ) → ( 𝑄 ∥ 𝑥 ∨ 𝑄 ∥ 𝑦 ) ) ↔ ( 𝑄 ∥ ( 𝑋 · 𝑦 ) → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑦 ) ) ) )
15 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
16 15 breq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑄 ∥ ( 𝑋 · 𝑦 ) ↔ 𝑄 ∥ ( 𝑋 · 𝑌 ) ) )
17 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑄 ∥ 𝑦 ↔ 𝑄 ∥ 𝑌 ) )
18 17 orbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑦 ) ↔ ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌 ) ) )
19 16 18 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑄 ∥ ( 𝑋 · 𝑦 ) → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑦 ) ) ↔ ( 𝑄 ∥ ( 𝑋 · 𝑌 ) → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌 ) ) ) )
20 6 2 eleqtrdi ⊢ ( 𝜑 → 𝑄 ∈ ( RPrime ‘ 𝑅 ) )
21 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
22 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
23 1 21 22 3 4 isrprm ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑄 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑄 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑄 ∥ ( 𝑥 · 𝑦 ) → ( 𝑄 ∥ 𝑥 ∨ 𝑄 ∥ 𝑦 ) ) ) ) )
24 23 simplbda ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑄 ∈ ( RPrime ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑄 ∥ ( 𝑥 · 𝑦 ) → ( 𝑄 ∥ 𝑥 ∨ 𝑄 ∥ 𝑦 ) ) )
25 5 20 24 syl2anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑄 ∥ ( 𝑥 · 𝑦 ) → ( 𝑄 ∥ 𝑥 ∨ 𝑄 ∥ 𝑦 ) ) )
26 14 19 25 7 8 rspc2dv ⊢ ( 𝜑 → ( 𝑄 ∥ ( 𝑋 · 𝑌 ) → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌 ) ) )
27 9 26 mpd ⊢ ( 𝜑 → ( 𝑄 ∥ 𝑋 ∨ 𝑄 ∥ 𝑌 ) )