irredneg

Description: The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredneg.n	$⊢ N = {inv}_{g} (R)$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		eqid	$⊢ 1_{R} = 1_{R}$
6		simpl	$⊢ (R \in Ring \land X \in I) \to R \in Ring$
7	1 3	irredcl	$⊢ X \in I \to X \in {Base}_{R}$
8	7	adantl	$⊢ (R \in Ring \land X \in I) \to X \in {Base}_{R}$
9	3 4 5 2 6 8	rngnegr	$⊢ (R \in Ring \land X \in I) \to X \cdot_{R} N (1_{R}) = N (X)$
10		eqid	$⊢ Unit (R) = Unit (R)$
11	10 5	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
12	10 2	unitnegcl	$⊢ (R \in Ring \land 1_{R} \in Unit (R)) \to N (1_{R}) \in Unit (R)$
13	11 12	mpdan	$⊢ R \in Ring \to N (1_{R}) \in Unit (R)$
14	13	adantr	$⊢ (R \in Ring \land X \in I) \to N (1_{R}) \in Unit (R)$
15	1 10 4	irredrmul	$⊢ (R \in Ring \land X \in I \land N (1_{R}) \in Unit (R)) \to X \cdot_{R} N (1_{R}) \in I$
16	14 15	mpd3an3	$⊢ (R \in Ring \land X \in I) \to X \cdot_{R} N (1_{R}) \in I$
17	9 16	eqeltrrd	$⊢ (R \in Ring \land X \in I) \to N (X) \in I$

Metamath Proof Explorer