Metamath Proof Explorer

Theorem nrgdomn

Description: A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nrgdomn 
|- ( R e. NrmRing -> ( R e. Domn <-> R e. NzRing ) )

Proof

Step Hyp Ref Expression
1 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
2 simpr 
 |-  ( ( R e. NrmRing /\ R e. NzRing ) -> R e. NzRing )
3 eqid 
 |-  ( norm ` R ) = ( norm ` R )
4 eqid 
 |-  ( AbsVal ` R ) = ( AbsVal ` R )
5 3 4 nrgabv 
 |-  ( R e. NrmRing -> ( norm ` R ) e. ( AbsVal ` R ) )
6 5 ne0d 
 |-  ( R e. NrmRing -> ( AbsVal ` R ) =/= (/) )
7 6 adantr 
 |-  ( ( R e. NrmRing /\ R e. NzRing ) -> ( AbsVal ` R ) =/= (/) )
8 4 abvn0b 
 |-  ( R e. Domn <-> ( R e. NzRing /\ ( AbsVal ` R ) =/= (/) ) )
9 2 7 8 sylanbrc 
 |-  ( ( R e. NrmRing /\ R e. NzRing ) -> R e. Domn )
10 9 ex 
 |-  ( R e. NrmRing -> ( R e. NzRing -> R e. Domn ) )
11 1 10 impbid2 
 |-  ( R e. NrmRing -> ( R e. Domn <-> R e. NzRing ) )