This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem drngunz

Description: A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011)

Ref Expression
Hypotheses drngunz.z 
|- .0. = ( 0g ` R )
drngunz.u 
|- .1. = ( 1r ` R )
Assertion drngunz 
|- ( R e. DivRing -> .1. =/= .0. )

Proof

Step Hyp Ref Expression
1 drngunz.z 
 |-  .0. = ( 0g ` R )
2 drngunz.u 
 |-  .1. = ( 1r ` R )
3 drngring 
 |-  ( R e. DivRing -> R e. Ring )
4 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
5 4 2 1unit 
 |-  ( R e. Ring -> .1. e. ( Unit ` R ) )
6 3 5 syl 
 |-  ( R e. DivRing -> .1. e. ( Unit ` R ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 7 4 1 drngunit 
 |-  ( R e. DivRing -> ( .1. e. ( Unit ` R ) <-> ( .1. e. ( Base ` R ) /\ .1. =/= .0. ) ) )
9 6 8 mpbid 
 |-  ( R e. DivRing -> ( .1. e. ( Base ` R ) /\ .1. =/= .0. ) )
10 9 simprd 
 |-  ( R e. DivRing -> .1. =/= .0. )