Theorem irredlmul

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

	Ref	Expression
Hypotheses	irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
	irredrmul.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	irredrmul.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	irredlmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	⊢ 𝐼 = ( Irred ‘ 𝑅 )
2		irredrmul.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		irredrmul.t	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
7	4 3 5 6	opprmul	⊢ ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑋 · 𝑌 )
8	5	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
9	5 1	opprirred	⊢ 𝐼 = ( Irred ‘ ( oppr ‘ 𝑅 ) )
10	2 5	opprunit	⊢ 𝑈 = ( Unit ‘ ( oppr ‘ 𝑅 ) )
11	9 10 6	irredrmul	⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
12	8 11	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
13	12	3com23	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑌 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) ∈ 𝐼 )
14	7 13	eqeltrrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝐼 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )