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

Metamath Proof Explorer

Theorem irredneg

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

Ref Expression
Hypotheses irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
irredneg.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion irredneg ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredneg.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑅 ∈ Ring )
7 1 3 irredcl ⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
8 7 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
9 3 4 5 2 6 8 ringnegr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ 𝑋 ) )
10 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
11 10 5 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
12 10 2 unitnegcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
13 11 12 mpdan ⊢ ( 𝑅 ∈ Ring → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
14 13 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
15 1 10 4 irredrmul ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ 𝐼 )
16 14 15 mpd3an3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ 𝐼 )
17 9 16 eqeltrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )