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 NrmRing R NzRing A X B 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 NrmRing R NzRing A X B U R NrmRing
6 simprl R NrmRing R NzRing A X B U A X
7 nrgring R NrmRing R Ring
8 7 ad2antrr R NrmRing R NzRing A X B U R Ring
9 simprr R NrmRing R NzRing A X B U B U
10 eqid inv r R = inv r R
11 3 10 1 ringinvcl R Ring B U inv r R B X
12 8 9 11 syl2anc R NrmRing R NzRing A X B U inv r R B X
13 eqid R = R
14 1 2 13 nmmul R NrmRing A X inv r R B X N A R inv r R B = N A N inv r R B
15 5 6 12 14 syl3anc R NrmRing R NzRing A X B U N A R inv r R B = N A N inv r R B
16 simplr R NrmRing R NzRing A X B U R NzRing
17 2 3 10 nminvr R NrmRing R NzRing B U N inv r R B = 1 N B
18 5 16 9 17 syl3anc R NrmRing R NzRing A X B U N inv r R B = 1 N B
19 18 oveq2d R NrmRing R NzRing A X B U N A N inv r R B = N A 1 N B
20 15 19 eqtrd R NrmRing R NzRing A X B U N A R inv r R B = N A 1 N B
21 1 13 3 10 4 dvrval A X B U A × ˙ B = A R inv r R B
22 21 adantl R NrmRing R NzRing A X B U A × ˙ B = A R inv r R B
23 22 fveq2d R NrmRing R NzRing A X B U N A × ˙ B = N A R inv r R B
24 nrgngp R NrmRing R NrmGrp
25 24 ad2antrr R NrmRing R NzRing A X B U R NrmGrp
26 1 2 nmcl R NrmGrp A X N A
27 25 6 26 syl2anc R NrmRing R NzRing A X B U N A
28 27 recnd R NrmRing R NzRing A X B U N A
29 1 3 unitss U X
30 29 9 sselid R NrmRing R NzRing A X B U B X
31 1 2 nmcl R NrmGrp B X N B
32 25 30 31 syl2anc R NrmRing R NzRing A X B U N B
33 32 recnd R NrmRing R NzRing A X B U N B
34 2 3 unitnmn0 R NrmRing R NzRing B U N B 0
35 34 3expa R NrmRing R NzRing B U N B 0
36 35 adantrl R NrmRing R NzRing A X B U N B 0
37 28 33 36 divrecd R NrmRing R NzRing A X B U N A N B = N A 1 N B
38 20 23 37 3eqtr4d R NrmRing R NzRing A X B U N A × ˙ B = N A N B