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 = {inv}_{g} (R)$
	irrednegb.b	$⊢ B = {Base}_{R}$
Assertion	irrednegb	$⊢ (R \in Ring \land X \in B) \to (X \in I \leftrightarrow N (X) \in I)$

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredneg.n	$⊢ N = {inv}_{g} (R)$
3		irrednegb.b	$⊢ B = {Base}_{R}$
4	1 2	irredneg	$⊢ (R \in Ring \land X \in I) \to N (X) \in I$
5	4	adantlr	$⊢ ((R \in Ring \land X \in B) \land X \in I) \to N (X) \in I$
6		ringgrp	$⊢ R \in Ring \to R \in Grp$
7	3 2	grpinvinv	$⊢ (R \in Grp \land X \in B) \to N (N (X)) = X$
8	6 7	sylan	$⊢ (R \in Ring \land X \in B) \to N (N (X)) = X$
9	8	adantr	$⊢ ((R \in Ring \land X \in B) \land N (X) \in I) \to N (N (X)) = X$
10	1 2	irredneg	$⊢ (R \in Ring \land N (X) \in I) \to N (N (X)) \in I$
11	10	adantlr	$⊢ ((R \in Ring \land X \in B) \land N (X) \in I) \to N (N (X)) \in I$
12	9 11	eqeltrrd	$⊢ ((R \in Ring \land X \in B) \land N (X) \in I) \to X \in I$
13	5 12	impbida	$⊢ (R \in Ring \land X \in B) \to (X \in I \leftrightarrow N (X) \in I)$

Metamath Proof Explorer