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 \in NrmRing \land R \in NzRing \land A \in U) \to N (I (A)) = \frac{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 \in NrmRing \to R \in NrmGrp$
5	4	3ad2ant1	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to R \in NrmGrp$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	6 2	unitcl	$⊢ A \in U \to A \in {Base}_{R}$
8	7	3ad2ant3	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to A \in {Base}_{R}$
9	6 1	nmcl	$⊢ (R \in NrmGrp \land A \in {Base}_{R}) \to N (A) \in ℝ$
10	5 8 9	syl2anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) \in ℝ$
11	10	recnd	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) \in ℂ$
12		nzrring	$⊢ R \in NzRing \to R \in Ring$
13	12	3ad2ant2	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to R \in Ring$
14		simp3	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to A \in U$
15	2 3 6	ringinvcl	$⊢ (R \in Ring \land A \in U) \to I (A) \in {Base}_{R}$
16	13 14 15	syl2anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to I (A) \in {Base}_{R}$
17	6 1	nmcl	$⊢ (R \in NrmGrp \land I (A) \in {Base}_{R}) \to N (I (A)) \in ℝ$
18	5 16 17	syl2anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (I (A)) \in ℝ$
19	18	recnd	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (I (A)) \in ℂ$
20	1 2	unitnmn0	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) \neq 0$
21		eqid	$⊢ \cdot_{R} = \cdot_{R}$
22		eqid	$⊢ 1_{R} = 1_{R}$
23	2 3 21 22	unitrinv	$⊢ (R \in Ring \land A \in U) \to A \cdot_{R} I (A) = 1_{R}$
24	13 14 23	syl2anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to A \cdot_{R} I (A) = 1_{R}$
25	24	fveq2d	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A \cdot_{R} I (A)) = N (1_{R})$
26		simp1	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to R \in NrmRing$
27	6 1 21	nmmul	$⊢ (R \in NrmRing \land A \in {Base}_{R} \land I (A) \in {Base}_{R}) \to N (A \cdot_{R} I (A)) = N (A) N (I (A))$
28	26 8 16 27	syl3anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A \cdot_{R} I (A)) = N (A) N (I (A))$
29	1 22	nm1	$⊢ (R \in NrmRing \land R \in NzRing) \to N (1_{R}) = 1$
30	29	3adant3	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (1_{R}) = 1$
31	25 28 30	3eqtr3d	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) N (I (A)) = 1$
32	11 19 20 31	mvllmuld	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (I (A)) = \frac{1}{N (A)}$

Metamath Proof Explorer

Theorem nminvr

Proof