Metamath Proof Explorer

Theorem nmdvr

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

Ref Expression
Hypotheses nmdvr.x 
|- X = ( Base ` R )
nmdvr.n 
|- N = ( norm ` R )
nmdvr.u 
|- U = ( Unit ` R )
nmdvr.d 
|- ./ = ( /r ` R )
Assertion nmdvr 
|- ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( ( N ` A ) / ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 nmdvr.x 
 |-  X = ( Base ` R )
2 nmdvr.n 
 |-  N = ( norm ` R )
3 nmdvr.u 
 |-  U = ( Unit ` R )
4 nmdvr.d 
 |-  ./ = ( /r ` R )
5 simpll 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NrmRing )
6 simprl 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> A e. X )
7 nrgring 
 |-  ( R e. NrmRing -> R e. Ring )
8 7 ad2antrr 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. Ring )
9 simprr 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> B e. U )
10 eqid 
 |-  ( invr ` R ) = ( invr ` R )
11 3 10 1 ringinvcl 
 |-  ( ( R e. Ring /\ B e. U ) -> ( ( invr ` R ) ` B ) e. X )
12 8 9 11 syl2anc 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( invr ` R ) ` B ) e. X )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 1 2 13 nmmul 
 |-  ( ( R e. NrmRing /\ A e. X /\ ( ( invr ` R ) ` B ) e. X ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) )
15 5 6 12 14 syl3anc 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) )
16 simplr 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NzRing )
17 2 3 10 nminvr 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ B e. U ) -> ( N ` ( ( invr ` R ) ` B ) ) = ( 1 / ( N ` B ) ) )
18 5 16 9 17 syl3anc 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( ( invr ` R ) ` B ) ) = ( 1 / ( N ` B ) ) )
19 18 oveq2d 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( N ` A ) x. ( N ` ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) )
20 15 19 eqtrd 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) )
21 1 13 3 10 4 dvrval 
 |-  ( ( A e. X /\ B e. U ) -> ( A ./ B ) = ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) )
22 21 adantl 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( A ./ B ) = ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) )
23 22 fveq2d 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( N ` ( A ( .r ` R ) ( ( invr ` R ) ` B ) ) ) )
24 nrgngp 
 |-  ( R e. NrmRing -> R e. NrmGrp )
25 24 ad2antrr 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> R e. NrmGrp )
26 1 2 nmcl 
 |-  ( ( R e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )
27 25 6 26 syl2anc 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` A ) e. RR )
28 27 recnd 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` A ) e. CC )
29 1 3 unitss 
 |-  U C_ X
30 29 9 sseldi 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> B e. X )
31 1 2 nmcl 
 |-  ( ( R e. NrmGrp /\ B e. X ) -> ( N ` B ) e. RR )
32 25 30 31 syl2anc 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) e. RR )
33 32 recnd 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) e. CC )
34 2 3 unitnmn0 
 |-  ( ( R e. NrmRing /\ R e. NzRing /\ B e. U ) -> ( N ` B ) =/= 0 )
35 34 3expa 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ B e. U ) -> ( N ` B ) =/= 0 )
36 35 adantrl 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` B ) =/= 0 )
37 28 33 36 divrecd 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( ( N ` A ) / ( N ` B ) ) = ( ( N ` A ) x. ( 1 / ( N ` B ) ) ) )
38 20 23 37 3eqtr4d 
 |-  ( ( ( R e. NrmRing /\ R e. NzRing ) /\ ( A e. X /\ B e. U ) ) -> ( N ` ( A ./ B ) ) = ( ( N ` A ) / ( N ` B ) ) )