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

Metamath Proof Explorer

Theorem nminvr

Description: The norm of an inverse 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 )
nminvr.i 
|- I = ( invr ` R )
Assertion nminvr 
|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) = ( 1 / ( N ` A ) ) )

Proof

Step Hyp Ref Expression
1 nminvr.n 
 |-  N = ( norm ` R )
2 nminvr.u 
 |-  U = ( Unit ` R )
3 nminvr.i 
 |-  I = ( invr ` R )
4 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
5 4 3ad2ant1 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. NrmGrp )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 6 2 unitcl 
 |-  ( A e. U -> A e. ( Base ` R ) )
8 7 3ad2ant3 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A e. ( Base ` R ) )
9 6 1 nmcl 
 |-  ( ( R e. NrmGrp /\ A e. ( Base ` R ) ) -> ( N ` A ) e. RR )
10 5 8 9 syl2anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) e. RR )
11 10 recnd 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) e. CC )
12 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
13 12 3ad2ant2 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. Ring )
14 simp3 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A e. U )
15 2 3 6 ringinvcl 
 |-  ( ( R e. Ring /\ A e. U ) -> ( I ` A ) e. ( Base ` R ) )
16 13 14 15 syl2anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( I ` A ) e. ( Base ` R ) )
17 6 1 nmcl 
 |-  ( ( R e. NrmGrp /\ ( I ` A ) e. ( Base ` R ) ) -> ( N ` ( I ` A ) ) e. RR )
18 5 16 17 syl2anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) e. RR )
19 18 recnd 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) e. CC )
20 1 2 unitnmn0 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) =/= 0 )
21 eqid 
 |-  ( .r ` R ) = ( .r ` R )
22 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
23 2 3 21 22 unitrinv 
 |-  ( ( R e. Ring /\ A e. U ) -> ( A ( .r ` R ) ( I ` A ) ) = ( 1r ` R ) )
24 13 14 23 syl2anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( A ( .r ` R ) ( I ` A ) ) = ( 1r ` R ) )
25 24 fveq2d 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( N ` ( 1r ` R ) ) )
26 simp1 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. NrmRing )
27 6 1 21 nmmul 
 |-  ( ( R e. NrmRing /\ A e. ( Base ` R ) /\ ( I ` A ) e. ( Base ` R ) ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( ( N ` A ) x. ( N ` ( I ` A ) ) ) )
28 26 8 16 27 syl3anc 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( ( N ` A ) x. ( N ` ( I ` A ) ) ) )
29 1 22 nm1 
 |-  ( ( R e. NrmRing /\ R e. NzRing ) -> ( N ` ( 1r ` R ) ) = 1 )
30 29 3adant3 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( 1r ` R ) ) = 1 )
31 25 28 30 3eqtr3d 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( ( N ` A ) x. ( N ` ( I ` A ) ) ) = 1 )
32 11 19 20 31 mvllmuld 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) = ( 1 / ( N ` A ) ) )