Theorem irrednegb

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

	Ref	Expression
Hypotheses	irredn0.i	|- I = ( Irred ` R )
	irredneg.n	|- N = ( invg ` R )
	irrednegb.b	|- B = ( Base ` R )
Assertion	irrednegb	|- ( ( R e. Ring /\ X e. B ) -> ( X e. I <-> ( N ` X ) e. I ) )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	|- I = ( Irred ` R )
2		irredneg.n	|- N = ( invg ` R )
3		irrednegb.b	|- B = ( Base ` R )
4	1 2	irredneg	|- ( ( R e. Ring /\ X e. I ) -> ( N ` X ) e. I )
5	4	adantlr	|- ( ( ( R e. Ring /\ X e. B ) /\ X e. I ) -> ( N ` X ) e. I )
6		ringgrp	|- ( R e. Ring -> R e. Grp )
7	3 2	grpinvinv	|- ( ( R e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
8	6 7	sylan	|- ( ( R e. Ring /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
9	8	adantr	|- ( ( ( R e. Ring /\ X e. B ) /\ ( N ` X ) e. I ) -> ( N ` ( N ` X ) ) = X )
10	1 2	irredneg	|- ( ( R e. Ring /\ ( N ` X ) e. I ) -> ( N ` ( N ` X ) ) e. I )
11	10	adantlr	|- ( ( ( R e. Ring /\ X e. B ) /\ ( N ` X ) e. I ) -> ( N ` ( N ` X ) ) e. I )
12	9 11	eqeltrrd	|- ( ( ( R e. Ring /\ X e. B ) /\ ( N ` X ) e. I ) -> X e. I )
13	5 12	impbida	|- ( ( R e. Ring /\ X e. B ) -> ( X e. I <-> ( N ` X ) e. I ) )