Metamath Proof Explorer

Theorem irredrmul

Description: The product of an irreducible element and a unit 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 irredrmul 
|- ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( 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 simp2 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> X e. I )
5 simp1 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> R e. Ring )
6 simp3 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> Y e. U )
7 eqid 
 |-  ( /r ` R ) = ( /r ` R )
8 2 7 unitdvcl 
 |-  ( ( R e. Ring /\ ( X .x. Y ) e. U /\ Y e. U ) -> ( ( X .x. Y ) ( /r ` R ) Y ) e. U )
9 8 3com23 
 |-  ( ( R e. Ring /\ Y e. U /\ ( X .x. Y ) e. U ) -> ( ( X .x. Y ) ( /r ` R ) Y ) e. U )
10 9 3expia 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( X .x. Y ) e. U -> ( ( X .x. Y ) ( /r ` R ) Y ) e. U ) )
11 5 6 10 syl2anc 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( ( X .x. Y ) e. U -> ( ( X .x. Y ) ( /r ` R ) Y ) e. U ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 1 12 irredcl 
 |-  ( X e. I -> X e. ( Base ` R ) )
14 13 3ad2ant2 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> X e. ( Base ` R ) )
15 12 2 7 3 dvrcan3 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Y e. U ) -> ( ( X .x. Y ) ( /r ` R ) Y ) = X )
16 5 14 6 15 syl3anc 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( ( X .x. Y ) ( /r ` R ) Y ) = X )
17 16 eleq1d 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( ( ( X .x. Y ) ( /r ` R ) Y ) e. U <-> X e. U ) )
18 11 17 sylibd 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( ( X .x. Y ) e. U -> X e. U ) )
19 5 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> R e. Ring )
20 eldifi 
 |-  ( y e. ( ( Base ` R ) \ U ) -> y e. ( Base ` R ) )
21 20 ad2antrl 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> y e. ( Base ` R ) )
22 6 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> Y e. U )
23 12 2 7 dvrcl 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) /\ Y e. U ) -> ( y ( /r ` R ) Y ) e. ( Base ` R ) )
24 19 21 22 23 syl3anc 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( y ( /r ` R ) Y ) e. ( Base ` R ) )
25 eldifn 
 |-  ( y e. ( ( Base ` R ) \ U ) -> -. y e. U )
26 25 ad2antrl 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> -. y e. U )
27 2 3 unitmulcl 
 |-  ( ( R e. Ring /\ ( y ( /r ` R ) Y ) e. U /\ Y e. U ) -> ( ( y ( /r ` R ) Y ) .x. Y ) e. U )
28 27 3com23 
 |-  ( ( R e. Ring /\ Y e. U /\ ( y ( /r ` R ) Y ) e. U ) -> ( ( y ( /r ` R ) Y ) .x. Y ) e. U )
29 28 3expia 
 |-  ( ( R e. Ring /\ Y e. U ) -> ( ( y ( /r ` R ) Y ) e. U -> ( ( y ( /r ` R ) Y ) .x. Y ) e. U ) )
30 19 22 29 syl2anc 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( y ( /r ` R ) Y ) e. U -> ( ( y ( /r ` R ) Y ) .x. Y ) e. U ) )
31 12 2 7 3 dvrcan1 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) /\ Y e. U ) -> ( ( y ( /r ` R ) Y ) .x. Y ) = y )
32 19 21 22 31 syl3anc 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( y ( /r ` R ) Y ) .x. Y ) = y )
33 32 eleq1d 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( ( y ( /r ` R ) Y ) .x. Y ) e. U <-> y e. U ) )
34 30 33 sylibd 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( y ( /r ` R ) Y ) e. U -> y e. U ) )
35 26 34 mtod 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> -. ( y ( /r ` R ) Y ) e. U )
36 24 35 eldifd 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( y ( /r ` R ) Y ) e. ( ( Base ` R ) \ U ) )
37 simprr 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( x .x. y ) = ( X .x. Y ) )
38 37 oveq1d 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( x .x. y ) ( /r ` R ) Y ) = ( ( X .x. Y ) ( /r ` R ) Y ) )
39 eldifi 
 |-  ( x e. ( ( Base ` R ) \ U ) -> x e. ( Base ` R ) )
40 39 ad2antlr 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> x e. ( Base ` R ) )
41 12 2 7 3 dvrass 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ Y e. U ) ) -> ( ( x .x. y ) ( /r ` R ) Y ) = ( x .x. ( y ( /r ` R ) Y ) ) )
42 19 40 21 22 41 syl13anc 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( x .x. y ) ( /r ` R ) Y ) = ( x .x. ( y ( /r ` R ) Y ) ) )
43 16 ad2antrr 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( ( X .x. Y ) ( /r ` R ) Y ) = X )
44 38 42 43 3eqtr3d 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> ( x .x. ( y ( /r ` R ) Y ) ) = X )
45 oveq2 
 |-  ( z = ( y ( /r ` R ) Y ) -> ( x .x. z ) = ( x .x. ( y ( /r ` R ) Y ) ) )
46 45 eqeq1d 
 |-  ( z = ( y ( /r ` R ) Y ) -> ( ( x .x. z ) = X <-> ( x .x. ( y ( /r ` R ) Y ) ) = X ) )
47 46 rspcev 
 |-  ( ( ( y ( /r ` R ) Y ) e. ( ( Base ` R ) \ U ) /\ ( x .x. ( y ( /r ` R ) Y ) ) = X ) -> E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X )
48 36 44 47 syl2anc 
 |-  ( ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) /\ ( y e. ( ( Base ` R ) \ U ) /\ ( x .x. y ) = ( X .x. Y ) ) ) -> E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X )
49 48 rexlimdvaa 
 |-  ( ( ( R e. Ring /\ X e. I /\ Y e. U ) /\ x e. ( ( Base ` R ) \ U ) ) -> ( E. y e. ( ( Base ` R ) \ U ) ( x .x. y ) = ( X .x. Y ) -> E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X ) )
50 49 reximdva 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( E. x e. ( ( Base ` R ) \ U ) E. y e. ( ( Base ` R ) \ U ) ( x .x. y ) = ( X .x. Y ) -> E. x e. ( ( Base ` R ) \ U ) E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X ) )
51 18 50 orim12d 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( ( ( X .x. Y ) e. U \/ E. x e. ( ( Base ` R ) \ U ) E. y e. ( ( Base ` R ) \ U ) ( x .x. y ) = ( X .x. Y ) ) -> ( X e. U \/ E. x e. ( ( Base ` R ) \ U ) E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X ) ) )
52 12 2 unitcl 
 |-  ( Y e. U -> Y e. ( Base ` R ) )
53 52 3ad2ant3 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> Y e. ( Base ` R ) )
54 12 3 ringcl 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) /\ Y e. ( Base ` R ) ) -> ( X .x. Y ) e. ( Base ` R ) )
55 5 14 53 54 syl3anc 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( X .x. Y ) e. ( Base ` R ) )
56 eqid 
 |-  ( ( Base ` R ) \ U ) = ( ( Base ` R ) \ U )
57 12 2 1 56 3 isnirred 
 |-  ( ( X .x. Y ) e. ( Base ` R ) -> ( -. ( X .x. Y ) e. I <-> ( ( X .x. Y ) e. U \/ E. x e. ( ( Base ` R ) \ U ) E. y e. ( ( Base ` R ) \ U ) ( x .x. y ) = ( X .x. Y ) ) ) )
58 55 57 syl 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( -. ( X .x. Y ) e. I <-> ( ( X .x. Y ) e. U \/ E. x e. ( ( Base ` R ) \ U ) E. y e. ( ( Base ` R ) \ U ) ( x .x. y ) = ( X .x. Y ) ) ) )
59 12 2 1 56 3 isnirred 
 |-  ( X e. ( Base ` R ) -> ( -. X e. I <-> ( X e. U \/ E. x e. ( ( Base ` R ) \ U ) E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X ) ) )
60 14 59 syl 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( -. X e. I <-> ( X e. U \/ E. x e. ( ( Base ` R ) \ U ) E. z e. ( ( Base ` R ) \ U ) ( x .x. z ) = X ) ) )
61 51 58 60 3imtr4d 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( -. ( X .x. Y ) e. I -> -. X e. I ) )
62 4 61 mt4d 
 |-  ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( X .x. Y ) e. I )