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 = ( invr ` R )
Assertion	nminvr	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. 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 = ( invr ` R )
4		nrgngp	\|- ( R e. NrmRing -> R e. NrmGrp )
5	4	3ad2ant1	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. NrmGrp )
6		eqid	\|- ( Base ` R ) = ( Base ` R )
7	6 2	unitcl	\|- ( A e. U -> A e. ( Base ` R ) )
8	7	3ad2ant3	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A e. ( Base ` R ) )
9	6 1	nmcl	\|- ( ( R e. NrmGrp /\ A e. ( Base ` R ) ) -> ( N ` A ) e. RR )
10	5 8 9	syl2anc	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) e. RR )
11	10	recnd	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) e. CC )
12		nzrring	\|- ( R e. NzRing -> R e. Ring )
13	12	3ad2ant2	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. Ring )
14		simp3	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> A e. U )
15	2 3 6	ringinvcl	\|- ( ( R e. Ring /\ A e. U ) -> ( I ` A ) e. ( Base ` R ) )
16	13 14 15	syl2anc	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( I ` A ) e. ( Base ` R ) )
17	6 1	nmcl	\|- ( ( R e. NrmGrp /\ ( I ` A ) e. ( Base ` R ) ) -> ( N ` ( I ` A ) ) e. RR )
18	5 16 17	syl2anc	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) e. RR )
19	18	recnd	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) e. CC )
20	1 2	unitnmn0	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` A ) =/= 0 )
21		eqid	\|- ( .r ` R ) = ( .r ` R )
22		eqid	\|- ( 1r ` R ) = ( 1r ` R )
23	2 3 21 22	unitrinv	\|- ( ( R e. Ring /\ A e. U ) -> ( A ( .r ` R ) ( I ` A ) ) = ( 1r ` R ) )
24	13 14 23	syl2anc	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( A ( .r ` R ) ( I ` A ) ) = ( 1r ` R ) )
25	24	fveq2d	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( N ` ( 1r ` R ) ) )
26		simp1	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> R e. NrmRing )
27	6 1 21	nmmul	\|- ( ( R e. NrmRing /\ A e. ( Base ` R ) /\ ( I ` A ) e. ( Base ` R ) ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( ( N ` A ) x. ( N ` ( I ` A ) ) ) )
28	26 8 16 27	syl3anc	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( A ( .r ` R ) ( I ` A ) ) ) = ( ( N ` A ) x. ( N ` ( I ` A ) ) ) )
29	1 22	nm1	\|- ( ( R e. NrmRing /\ R e. NzRing ) -> ( N ` ( 1r ` R ) ) = 1 )
30	29	3adant3	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( 1r ` R ) ) = 1 )
31	25 28 30	3eqtr3d	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( ( N ` A ) x. ( N ` ( I ` A ) ) ) = 1 )
32	11 19 20 31	mvllmuld	\|- ( ( R e. NrmRing /\ R e. NzRing /\ A e. U ) -> ( N ` ( I ` A ) ) = ( 1 / ( N ` A ) ) )

Metamath Proof Explorer

Theorem nminvr

Proof