This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem irredlmul

Description: The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
irredrmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
irredrmul.t ⊢ · = ( .r ‘ 𝑅 )
Assertion irredlmul ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredrmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 irredrmul.t ⊢ · = ( .r ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
7 4 3 5 6 opprmul ⊢ ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · 𝑌 )
8 5 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
9 5 1 opprirred ⊢ 𝐼 = ( Irred ‘ ( oppr ‘ 𝑅 ) )
10 2 5 opprunit ⊢ 𝑈 = ( Unit ‘ ( oppr ‘ 𝑅 ) )
11 9 10 6 irredrmul ⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
12 8 11 syl3an1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
13 12 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
14 7 13 eqeltrrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )