Theorem irredneg

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

	Ref	Expression
Hypotheses	irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irredneg.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion	irredneg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irredneg.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑅 ∈ Ring )
7	1 3	irredcl	⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
8	7	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
9	3 4 5 2 6 8	ringnegr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ 𝑋 ) )
10		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
11	10 5	1unit	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
12	10 2	unitnegcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
13	11 12	mpdan	⊢ ( 𝑅 ∈ Ring → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
14	13	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
15	1 10 4	irredrmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ 𝐼 )
16	14 15	mpd3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ∈ 𝐼 )
17	9 16	eqeltrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐼 )