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	⊢ 𝑁 = ( norm ‘ 𝑅 )
	nminvr.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	nminvr.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion	nminvr	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 1 / ( 𝑁 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nminvr.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
2		nminvr.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		nminvr.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
4		nrgngp	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
5	4	3ad2ant1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ NrmGrp )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	6 2	unitcl	⊢ ( 𝐴 ∈ 𝑈 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
8	7	3ad2ant3	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
9	6 1	nmcl	⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
10	5 8 9	syl2anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
11	10	recnd	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ )
12		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
13	12	3ad2ant2	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ Ring )
14		simp3	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ 𝑈 )
15	2 3 6	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ) → ( 𝐼 ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
16	13 14 15	syl2anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝐼 ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
17	6 1	nmcl	⊢ ( ( 𝑅 ∈ NrmGrp ∧ ( 𝐼 ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℝ )
18	5 16 17	syl2anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℝ )
19	18	recnd	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ∈ ℂ )
20	1 2	unitnmn0	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )
21		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
22		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
23	2 3 21 22	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
24	13 14 23	syl2anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
25	24	fveq2d	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝐴 ) ) ) = ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) )
26		simp1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ NrmRing )
27	6 1 21	nmmul	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐼 ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ) )
28	26 8 16 27	syl3anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐴 ( .r ‘ 𝑅 ) ( 𝐼 ‘ 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ) )
29	1 22	nm1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
30	29	3adant3	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
31	25 28 30	3eqtr3d	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) ) = 1 )
32	11 19 20 31	mvllmuld	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝐼 ‘ 𝐴 ) ) = ( 1 / ( 𝑁 ‘ 𝐴 ) ) )