Metamath Proof Explorer


Theorem nminvr

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

Ref Expression
Hypotheses nminvr.n N = norm R
nminvr.u U = Unit R
nminvr.i I = inv r R
Assertion nminvr R NrmRing R NzRing A U N I A = 1 N A

Proof

Step Hyp Ref Expression
1 nminvr.n N = norm R
2 nminvr.u U = Unit R
3 nminvr.i I = inv r R
4 nrgngp R NrmRing R NrmGrp
5 4 3ad2ant1 R NrmRing R NzRing A U R NrmGrp
6 eqid Base R = Base R
7 6 2 unitcl A U A Base R
8 7 3ad2ant3 R NrmRing R NzRing A U A Base R
9 6 1 nmcl R NrmGrp A Base R N A
10 5 8 9 syl2anc R NrmRing R NzRing A U N A
11 10 recnd R NrmRing R NzRing A U N A
12 nzrring R NzRing R Ring
13 12 3ad2ant2 R NrmRing R NzRing A U R Ring
14 simp3 R NrmRing R NzRing A U A U
15 2 3 6 ringinvcl R Ring A U I A Base R
16 13 14 15 syl2anc R NrmRing R NzRing A U I A Base R
17 6 1 nmcl R NrmGrp I A Base R N I A
18 5 16 17 syl2anc R NrmRing R NzRing A U N I A
19 18 recnd R NrmRing R NzRing A U N I A
20 1 2 unitnmn0 R NrmRing R NzRing A U N A 0
21 eqid R = R
22 eqid 1 R = 1 R
23 2 3 21 22 unitrinv R Ring A U A R I A = 1 R
24 13 14 23 syl2anc R NrmRing R NzRing A U A R I A = 1 R
25 24 fveq2d R NrmRing R NzRing A U N A R I A = N 1 R
26 simp1 R NrmRing R NzRing A U R NrmRing
27 6 1 21 nmmul R NrmRing A Base R I A Base R N A R I A = N A N I A
28 26 8 16 27 syl3anc R NrmRing R NzRing A U N A R I A = N A N I A
29 1 22 nm1 R NrmRing R NzRing N 1 R = 1
30 29 3adant3 R NrmRing R NzRing A U N 1 R = 1
31 25 28 30 3eqtr3d R NrmRing R NzRing A U N A N I A = 1
32 11 19 20 31 mvllmuld R NrmRing R NzRing A U N I A = 1 N A