Metamath Proof Explorer

Theorem isngp

Description: The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses isngp.n ⊢ N = norm ⁡ G
isngp.z ⊢ - ˙ = - G
isngp.d ⊢ D = dist ⁡ G
Assertion isngp ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D

Proof

Step Hyp Ref Expression
1 isngp.n ⊢ N = norm ⁡ G
2 isngp.z ⊢ - ˙ = - G
3 isngp.d ⊢ D = dist ⁡ G
4 elin ⊢ G ∈ Grp ∩ MetSp ↔ G ∈ Grp ∧ G ∈ MetSp
5 4 anbi1i ⊢ G ∈ Grp ∩ MetSp ∧ N ∘ - ˙ ⊆ D ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
6 fveq2 ⊢ g = G → norm ⁡ g = norm ⁡ G
7 6 1 eqtr4di ⊢ g = G → norm ⁡ g = N
8 fveq2 ⊢ g = G → - g = - G
9 8 2 eqtr4di ⊢ g = G → - g = - ˙
10 7 9 coeq12d ⊢ g = G → norm ⁡ g ∘ - g = N ∘ - ˙
11 fveq2 ⊢ g = G → dist ⁡ g = dist ⁡ G
12 11 3 eqtr4di ⊢ g = G → dist ⁡ g = D
13 10 12 sseq12d ⊢ g = G → norm ⁡ g ∘ - g ⊆ dist ⁡ g ↔ N ∘ - ˙ ⊆ D
14 df-ngp ⊢ NrmGrp = g ∈ Grp ∩ MetSp | norm ⁡ g ∘ - g ⊆ dist ⁡ g
15 13 14 elrab2 ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∩ MetSp ∧ N ∘ - ˙ ⊆ D
16 df-3an ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
17 5 15 16 3bitr4i ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D