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 ∧ 𝑋𝐵 ) → ( 𝑋𝐼 ↔ ( 𝑁𝑋 ) ∈ 𝐼 ) )