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

Metamath Proof Explorer

Theorem irrednegb

Description: An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredneg.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
3 irrednegb.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 1 2 irredneg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )
5 4 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )
6 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7 3 2 grpinvinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
8 6 7 sylan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
10 1 2 irredneg ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐼 )
11 10 adantlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐼 )
12 9 11 eqeltrrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) → 𝑋 ∈ 𝐼 )
13 5 12 impbida ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐼 ↔ ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 ) )