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 sselid
 |-  ( ( ( 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 ) ) )