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