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 sseldi ⊢ ( ( ( 𝑅 ∈ 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 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈 ) ) → ( 𝑁 ‘ ( 𝐴 / 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) / ( 𝑁 ‘ 𝐵 ) ) )