Theorem tngngpd

Description: Derive the axioms for a normed group from the axioms for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	tngngp.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
	tngngp.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	tngngp.m	⊢ − = ( -g ‘ 𝐺 )
	tngngp.z	⊢ 0 = ( 0g ‘ 𝐺 )
	tngngpd.1	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	tngngpd.2	⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ ℝ )
	tngngpd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
	tngngpd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
Assertion	tngngpd	⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )

Proof

Step	Hyp	Ref	Expression
1		tngngp.t	⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2		tngngp.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
3		tngngp.m	⊢ − = ( -g ‘ 𝐺 )
4		tngngp.z	⊢ 0 = ( 0g ‘ 𝐺 )
5		tngngpd.1	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6		tngngpd.2	⊢ ( 𝜑 → 𝑁 : 𝑋 ⟶ ℝ )
7		tngngpd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
8		tngngpd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
9	2	fvexi	⊢ 𝑋 ∈ V
10		reex	⊢ ℝ ∈ V
11		fex2	⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V ) → 𝑁 ∈ V )
12	9 10 11	mp3an23	⊢ ( 𝑁 : 𝑋 ⟶ ℝ → 𝑁 ∈ V )
13	1 3	tngds	⊢ ( 𝑁 ∈ V → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
14	6 12 13	3syl	⊢ ( 𝜑 → ( 𝑁 ∘ − ) = ( dist ‘ 𝑇 ) )
15	2 3 4 5 6 7 8	nrmmetd	⊢ ( 𝜑 → ( 𝑁 ∘ − ) ∈ ( Met ‘ 𝑋 ) )
16	14 15	eqeltrrd	⊢ ( 𝜑 → ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) )
17		eqid	⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
18	1 2 17	tngngp2	⊢ ( 𝑁 : 𝑋 ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) ) ) )
19	6 18	syl	⊢ ( 𝜑 → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ 𝑋 ) ) ) )
20	5 16 19	mpbir2and	⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )