Metamath Proof Explorer

Theorem unitnmn0

Description: The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nminvr.n 
|- N = ( norm ` R )
nminvr.u 
|- U = ( Unit ` R )
Assertion unitnmn0 
|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 nminvr.n 
 |-  N = ( norm ` R )
2 nminvr.u 
 |-  U = ( Unit ` R )
3 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
4 3 3ad2ant1 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. NrmGrp )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 2 unitcl 
 |-  ( A e. U -> A e. ( Base ` R ) )
7 6 3ad2ant3 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A e. ( Base ` R ) )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 2 8 nzrunit 
 |-  ( ( R e. NzRing /\ A e. U ) -> A =/= ( 0g ` R ) )
10 9 3adant1 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A =/= ( 0g ` R ) )
11 5 1 8 nmne0 
 |-  ( ( R e. NrmGrp /\ A e. ( Base ` R ) /\ A =/= ( 0g ` R ) ) -> ( N ` A ) =/= 0 )
12 4 7 10 11 syl3anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) =/= 0 )