This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑁 = ( norm ‘ 𝐺 )
isngp.z ⊢ − = ( -g ‘ 𝐺 )
isngp.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion isngp ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 isngp.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
2 isngp.z ⊢ − = ( -g ‘ 𝐺 )
3 isngp.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 elin ⊢ ( 𝐺 ∈ ( Grp ∩ MetSp ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) )
5 4 anbi1i ⊢ ( ( 𝐺 ∈ ( Grp ∩ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( norm ‘ 𝑔 ) = ( norm ‘ 𝐺 ) )
7 6 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( norm ‘ 𝑔 ) = 𝑁 )
8 fveq2 ⊢ ( 𝑔 = 𝐺 → ( -g ‘ 𝑔 ) = ( -g ‘ 𝐺 ) )
9 8 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( -g ‘ 𝑔 ) = − )
10 7 9 coeq12d ⊢ ( 𝑔 = 𝐺 → ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) = ( 𝑁 ∘ − ) )
11 fveq2 ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) )
12 11 3 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = 𝐷 )
13 10 12 sseq12d ⊢ ( 𝑔 = 𝐺 → ( ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) ↔ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
14 df-ngp ⊢ NrmGrp = { 𝑔 ∈ ( Grp ∩ MetSp ) ∣ ( ( norm ‘ 𝑔 ) ∘ ( -g ‘ 𝑔 ) ) ⊆ ( dist ‘ 𝑔 ) }
15 13 14 elrab2 ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ ( Grp ∩ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
16 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
17 5 15 16 3bitr4i ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )