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	$⊢ I = Irred (R)$
	irredrmul.u	$⊢ U = Unit (R)$
	irredrmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	irredlmul	$⊢ (R \in Ring \land X \in U \land Y \in I) \to X \underset{˙}{\cdot} Y \in I$

Step	Hyp	Ref	Expression
1		irredn0.i	$⊢ I = Irred (R)$
2		irredrmul.u	$⊢ U = Unit (R)$
3		irredrmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
6		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
7	4 3 5 6	opprmul	$⊢ Y \cdot_{{opp}_{r} (R)} X = X \underset{˙}{\cdot} Y$
8	5	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
9	5 1	opprirred	$⊢ I = Irred ({opp}_{r} (R))$
10	2 5	opprunit	$⊢ U = Unit ({opp}_{r} (R))$
11	9 10 6	irredrmul	$⊢ ({opp}_{r} (R) \in Ring \land Y \in I \land X \in U) \to Y \cdot_{{opp}_{r} (R)} X \in I$
12	8 11	syl3an1	$⊢ (R \in Ring \land Y \in I \land X \in U) \to Y \cdot_{{opp}_{r} (R)} X \in I$
13	12	3com23	$⊢ (R \in Ring \land X \in U \land Y \in I) \to Y \cdot_{{opp}_{r} (R)} X \in I$
14	7 13	eqeltrrid	$⊢ (R \in Ring \land X \in U \land Y \in I) \to X \underset{˙}{\cdot} Y \in I$

Metamath Proof Explorer