Metamath Proof Explorer

Theorem irredn0

Description: The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i 
|- I = ( Irred ` R )
irredn0.z 
|- .0. = ( 0g ` R )
Assertion irredn0 
|- ( ( R e. Ring /\ X e. I ) -> X =/= .0. )

Proof

Step Hyp Ref Expression
1 irredn0.i 
 |-  I = ( Irred ` R )
2 irredn0.z 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 2 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
5 4 anim1i 
 |-  ( ( R e. Ring /\ -. .0. e. ( Unit ` R ) ) -> ( .0. e. ( Base ` R ) /\ -. .0. e. ( Unit ` R ) ) )
6 eldif 
 |-  ( .0. e. ( ( Base ` R ) \ ( Unit ` R ) ) <-> ( .0. e. ( Base ` R ) /\ -. .0. e. ( Unit ` R ) ) )
7 5 6 sylibr 
 |-  ( ( R e. Ring /\ -. .0. e. ( Unit ` R ) ) -> .0. e. ( ( Base ` R ) \ ( Unit ` R ) ) )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 3 8 2 ringlz 
 |-  ( ( R e. Ring /\ .0. e. ( Base ` R ) ) -> ( .0. ( .r ` R ) .0. ) = .0. )
10 4 9 mpdan 
 |-  ( R e. Ring -> ( .0. ( .r ` R ) .0. ) = .0. )
11 10 adantr 
 |-  ( ( R e. Ring /\ -. .0. e. ( Unit ` R ) ) -> ( .0. ( .r ` R ) .0. ) = .0. )
12 oveq1 
 |-  ( x = .0. -> ( x ( .r ` R ) y ) = ( .0. ( .r ` R ) y ) )
13 12 eqeq1d 
 |-  ( x = .0. -> ( ( x ( .r ` R ) y ) = .0. <-> ( .0. ( .r ` R ) y ) = .0. ) )
14 oveq2 
 |-  ( y = .0. -> ( .0. ( .r ` R ) y ) = ( .0. ( .r ` R ) .0. ) )
15 14 eqeq1d 
 |-  ( y = .0. -> ( ( .0. ( .r ` R ) y ) = .0. <-> ( .0. ( .r ` R ) .0. ) = .0. ) )
16 13 15 rspc2ev 
 |-  ( ( .0. e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ .0. e. ( ( Base ` R ) \ ( Unit ` R ) ) /\ ( .0. ( .r ` R ) .0. ) = .0. ) -> E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. )
17 7 7 11 16 syl3anc 
 |-  ( ( R e. Ring /\ -. .0. e. ( Unit ` R ) ) -> E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. )
18 17 ex 
 |-  ( R e. Ring -> ( -. .0. e. ( Unit ` R ) -> E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. ) )
19 18 orrd 
 |-  ( R e. Ring -> ( .0. e. ( Unit ` R ) \/ E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. ) )
20 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
21 eqid 
 |-  ( ( Base ` R ) \ ( Unit ` R ) ) = ( ( Base ` R ) \ ( Unit ` R ) )
22 3 20 1 21 8 isnirred 
 |-  ( .0. e. ( Base ` R ) -> ( -. .0. e. I <-> ( .0. e. ( Unit ` R ) \/ E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. ) ) )
23 4 22 syl 
 |-  ( R e. Ring -> ( -. .0. e. I <-> ( .0. e. ( Unit ` R ) \/ E. x e. ( ( Base ` R ) \ ( Unit ` R ) ) E. y e. ( ( Base ` R ) \ ( Unit ` R ) ) ( x ( .r ` R ) y ) = .0. ) ) )
24 19 23 mpbird 
 |-  ( R e. Ring -> -. .0. e. I )
25 24 adantr 
 |-  ( ( R e. Ring /\ X e. I ) -> -. .0. e. I )
26 simpr 
 |-  ( ( R e. Ring /\ X e. I ) -> X e. I )
27 eleq1 
 |-  ( X = .0. -> ( X e. I <-> .0. e. I ) )
28 26 27 syl5ibcom 
 |-  ( ( R e. Ring /\ X e. I ) -> ( X = .0. -> .0. e. I ) )
29 28 necon3bd 
 |-  ( ( R e. Ring /\ X e. I ) -> ( -. .0. e. I -> X =/= .0. ) )
30 25 29 mpd 
 |-  ( ( R e. Ring /\ X e. I ) -> X =/= .0. )