Metamath Proof Explorer

Theorem 0ringdif

Description: A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
Assertion 0ringdif 
|- ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )

Proof

Step Hyp Ref Expression
1 0ring.b 
 |-  B = ( Base ` R )
2 0ring.0 
 |-  .0. = ( 0g ` R )
3 eldif 
 |-  ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ -. R e. NzRing ) )
4 1 a1i 
 |-  ( R e. Ring -> B = ( Base ` R ) )
5 4 fveqeq2d 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 <-> ( # ` ( Base ` R ) ) = 1 ) )
6 1 2 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
7 6 ex 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 -> B = { .0. } ) )
8 fveq2 
 |-  ( B = { .0. } -> ( # ` B ) = ( # ` { .0. } ) )
9 2 fvexi 
 |-  .0. e. _V
10 hashsng 
 |-  ( .0. e. _V -> ( # ` { .0. } ) = 1 )
11 9 10 ax-mp 
 |-  ( # ` { .0. } ) = 1
12 8 11 eqtrdi 
 |-  ( B = { .0. } -> ( # ` B ) = 1 )
13 7 12 impbid1 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 <-> B = { .0. } ) )
14 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
15 5 13 14 3bitr3rd 
 |-  ( R e. Ring -> ( -. R e. NzRing <-> B = { .0. } ) )
16 15 pm5.32i 
 |-  ( ( R e. Ring /\ -. R e. NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )
17 3 16 bitri 
 |-  ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ B = { .0. } ) )