Metamath Proof Explorer

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 
|- I = ( Irred ` R )
irredrmul.u 
|- U = ( Unit ` R )
irredrmul.t 
|- .x. = ( .r ` R )
Assertion irredlmul 
|- ( ( R e. Ring /\ X e. U /\ Y e. I ) -> ( X .x. Y ) e. I )

Proof

Step Hyp Ref Expression
1 irredn0.i 
 |-  I = ( Irred ` R )
2 irredrmul.u 
 |-  U = ( Unit ` R )
3 irredrmul.t 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
6 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
7 4 3 5 6 opprmul 
 |-  ( Y ( .r ` ( oppR ` R ) ) X ) = ( X .x. Y )
8 5 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
9 5 1 opprirred 
 |-  I = ( Irred ` ( oppR ` R ) )
10 2 5 opprunit 
 |-  U = ( Unit ` ( oppR ` R ) )
11 9 10 6 irredrmul 
 |-  ( ( ( oppR ` R ) e. Ring /\ Y e. I /\ X e. U ) -> ( Y ( .r ` ( oppR ` R ) ) X ) e. I )
12 8 11 syl3an1 
 |-  ( ( R e. Ring /\ Y e. I /\ X e. U ) -> ( Y ( .r ` ( oppR ` R ) ) X ) e. I )
13 12 3com23 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. I ) -> ( Y ( .r ` ( oppR ` R ) ) X ) e. I )
14 7 13 eqeltrrid 
 |-  ( ( R e. Ring /\ X e. U /\ Y e. I ) -> ( X .x. Y ) e. I )