tngnrg

Description: Given any absolute value over a ring, augmenting the ring with the absolute value produces a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	tngnrg.t	$⊢ T = R toNrmGrp F$
	tngnrg.a	$⊢ A = AbsVal (R)$
Assertion	tngnrg	$⊢ F \in A \to T \in NrmRing$

Proof

Step	Hyp	Ref	Expression
1		tngnrg.t	$⊢ T = R toNrmGrp F$
2		tngnrg.a	$⊢ A = AbsVal (R)$
3	2	abvrcl	$⊢ F \in A \to R \in Ring$
4		ringgrp	$⊢ R \in Ring \to R \in Grp$
5	3 4	syl	$⊢ F \in A \to R \in Grp$
6		eqid	$⊢ -_{R} = -_{R}$
7	1 6	tngds	$⊢ F \in A \to F \circ -_{R} = dist (T)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8 2 6	abvmet	$⊢ F \in A \to F \circ -_{R} \in Met ({Base}_{R})$
10	7 9	eqeltrrd	$⊢ F \in A \to dist (T) \in Met ({Base}_{R})$
11	2 8	abvf	$⊢ F \in A \to F : {Base}_{R} ⟶ ℝ$
12		eqid	$⊢ dist (T) = dist (T)$
13	1 8 12	tngngp2	$⊢ F : {Base}_{R} ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (R \in Grp \land dist (T) \in Met ({Base}_{R})))$
14	11 13	syl	$⊢ F \in A \to (T \in NrmGrp \leftrightarrow (R \in Grp \land dist (T) \in Met ({Base}_{R})))$
15	5 10 14	mpbir2and	$⊢ F \in A \to T \in NrmGrp$
16		reex	$⊢ ℝ \in V$
17	1 8 16	tngnm	$⊢ (R \in Grp \land F : {Base}_{R} ⟶ ℝ) \to F = norm (T)$
18	5 11 17	syl2anc	$⊢ F \in A \to F = norm (T)$
19		eqidd	$⊢ F \in A \to {Base}_{R} = {Base}_{R}$
20	1 8	tngbas	$⊢ F \in A \to {Base}_{R} = {Base}_{T}$
21		eqid	$⊢ +_{R} = +_{R}$
22	1 21	tngplusg	$⊢ F \in A \to +_{R} = +_{T}$
23	22	oveqdr	$⊢ (F \in A \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x +_{R} y = x +_{T} y$
24		eqid	$⊢ \cdot_{R} = \cdot_{R}$
25	1 24	tngmulr	$⊢ F \in A \to \cdot_{R} = \cdot_{T}$
26	25	oveqdr	$⊢ (F \in A \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \cdot_{R} y = x \cdot_{T} y$
27	19 20 23 26	abvpropd	$⊢ F \in A \to AbsVal (R) = AbsVal (T)$
28	2 27	eqtrid	$⊢ F \in A \to A = AbsVal (T)$
29	18 28	eleq12d	$⊢ F \in A \to (F \in A \leftrightarrow norm (T) \in AbsVal (T))$
30	29	ibi	$⊢ F \in A \to norm (T) \in AbsVal (T)$
31		eqid	$⊢ norm (T) = norm (T)$
32		eqid	$⊢ AbsVal (T) = AbsVal (T)$
33	31 32	isnrg	$⊢ T \in NrmRing \leftrightarrow (T \in NrmGrp \land norm (T) \in AbsVal (T))$
34	15 30 33	sylanbrc	$⊢ F \in A \to T \in NrmRing$

Metamath Proof Explorer

Theorem tngnrg

Proof