Metamath Proof Explorer

Theorem irredmul

Description: If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
irredmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
irredmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
irredmul.t ⊢ · = ( .r ‘ 𝑅 )
Assertion irredmul ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐼 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 irredmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
4 irredmul.t ⊢ · = ( .r ‘ 𝑅 )
5 2 3 1 4 isirred2 ⊢ ( ( 𝑋 · 𝑌 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ¬ ( 𝑋 · 𝑌 ) ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
6 5 simp3bi ⊢ ( ( 𝑋 · 𝑌 ) ∈ 𝐼 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
7 eqid ⊢ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 )
8 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑦 ) )
9 8 eqeq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ↔ ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) )
10 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
11 10 orbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ↔ ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
12 9 11 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
14 13 eqeq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) ↔ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) ) )
15 eleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )
16 15 orbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ↔ ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
17 14 16 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ↔ ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) ) )
18 12 17 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑌 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) ) )
19 7 18 mpii ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
20 6 19 syl5 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝐼 → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) ) )
21 20 3impia ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 · 𝑌 ) ∈ 𝐼 ) → ( 𝑋 ∈ 𝑈 ∨ 𝑌 ∈ 𝑈 ) )