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 𝑋 = ( Base ‘ 𝑅 )
nmdvr.n 𝑁 = ( norm ‘ 𝑅 )
nmdvr.u 𝑈 = ( Unit ‘ 𝑅 )
nmdvr.d / = ( /r𝑅 )
Assertion nmdvr ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝑁𝐴 ) / ( 𝑁𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nmdvr.x 𝑋 = ( Base ‘ 𝑅 )
2 nmdvr.n 𝑁 = ( norm ‘ 𝑅 )
3 nmdvr.u 𝑈 = ( Unit ‘ 𝑅 )
4 nmdvr.d / = ( /r𝑅 )
5 simpll ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝑅 ∈ NrmRing )
6 simprl ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝐴𝑋 )
7 nrgring ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )
8 7 ad2antrr ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝑅 ∈ Ring )
9 simprr ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝐵𝑈 )
10 eqid ( invr𝑅 ) = ( invr𝑅 )
11 3 10 1 ringinvcl ( ( 𝑅 ∈ Ring ∧ 𝐵𝑈 ) → ( ( invr𝑅 ) ‘ 𝐵 ) ∈ 𝑋 )
12 8 9 11 syl2anc ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( ( invr𝑅 ) ‘ 𝐵 ) ∈ 𝑋 )
13 eqid ( .r𝑅 ) = ( .r𝑅 )
14 1 2 13 nmmul ( ( 𝑅 ∈ NrmRing ∧ 𝐴𝑋 ∧ ( ( invr𝑅 ) ‘ 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁𝐴 ) · ( 𝑁 ‘ ( ( invr𝑅 ) ‘ 𝐵 ) ) ) )
15 5 6 12 14 syl3anc ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁𝐴 ) · ( 𝑁 ‘ ( ( invr𝑅 ) ‘ 𝐵 ) ) ) )
16 simplr ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝑅 ∈ NzRing )
17 2 3 10 nminvr ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵𝑈 ) → ( 𝑁 ‘ ( ( invr𝑅 ) ‘ 𝐵 ) ) = ( 1 / ( 𝑁𝐵 ) ) )
18 5 16 9 17 syl3anc ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( ( invr𝑅 ) ‘ 𝐵 ) ) = ( 1 / ( 𝑁𝐵 ) ) )
19 18 oveq2d ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( ( 𝑁𝐴 ) · ( 𝑁 ‘ ( ( invr𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁𝐴 ) · ( 1 / ( 𝑁𝐵 ) ) ) )
20 15 19 eqtrd ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) ) = ( ( 𝑁𝐴 ) · ( 1 / ( 𝑁𝐵 ) ) ) )
21 1 13 3 10 4 dvrval ( ( 𝐴𝑋𝐵𝑈 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) )
22 21 adantl ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) )
23 22 fveq2d ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( 𝑁 ‘ ( 𝐴 ( .r𝑅 ) ( ( invr𝑅 ) ‘ 𝐵 ) ) ) )
24 nrgngp ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
25 24 ad2antrr ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝑅 ∈ NrmGrp )
26 1 2 nmcl ( ( 𝑅 ∈ NrmGrp ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) ∈ ℝ )
27 25 6 26 syl2anc ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁𝐴 ) ∈ ℝ )
28 27 recnd ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁𝐴 ) ∈ ℂ )
29 1 3 unitss 𝑈𝑋
30 29 9 sselid ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → 𝐵𝑋 )
31 1 2 nmcl ( ( 𝑅 ∈ NrmGrp ∧ 𝐵𝑋 ) → ( 𝑁𝐵 ) ∈ ℝ )
32 25 30 31 syl2anc ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁𝐵 ) ∈ ℝ )
33 32 recnd ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁𝐵 ) ∈ ℂ )
34 2 3 unitnmn0 ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵𝑈 ) → ( 𝑁𝐵 ) ≠ 0 )
35 34 3expa ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ 𝐵𝑈 ) → ( 𝑁𝐵 ) ≠ 0 )
36 35 adantrl ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁𝐵 ) ≠ 0 )
37 28 33 36 divrecd ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( ( 𝑁𝐴 ) / ( 𝑁𝐵 ) ) = ( ( 𝑁𝐴 ) · ( 1 / ( 𝑁𝐵 ) ) ) )
38 20 23 37 3eqtr4d ( ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) ∧ ( 𝐴𝑋𝐵𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝑁𝐴 ) / ( 𝑁𝐵 ) ) )