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 ⊢ 𝑁 = ( 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 / ( 𝑁 ‘ 𝐴 ) ) )