Metamath Proof Explorer

Theorem isngp3

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

Ref Expression
Hypotheses isngp.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
isngp.z ⊢ − = ( -g ‘ 𝐺 )
isngp.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
isngp2.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion isngp3 ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isngp.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
2 isngp.z ⊢ − = ( -g ‘ 𝐺 )
3 isngp.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 isngp2.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
5 eqid ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6 1 2 3 4 5 isngp2 ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) )
7 4 3 msmet2 ⊢ ( 𝐺 ∈ MetSp → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
8 1 4 3 5 nmf2 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) ) → 𝑁 : 𝑋 ⟶ ℝ )
9 7 8 sylan2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → 𝑁 : 𝑋 ⟶ ℝ )
10 4 2 grpsubf ⊢ ( 𝐺 ∈ Grp → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
11 10 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
12 fco ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
13 9 11 12 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
14 13 ffnd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( 𝑁 ∘ − ) Fn ( 𝑋 × 𝑋 ) )
15 7 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
16 metf ⊢ ( ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
17 ffn ⊢ ( ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) : ( 𝑋 × 𝑋 ) ⟶ ℝ → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) Fn ( 𝑋 × 𝑋 ) )
18 15 16 17 3syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) Fn ( 𝑋 × 𝑋 ) )
19 eqfnov2 ⊢ ( ( ( 𝑁 ∘ − ) Fn ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) Fn ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) ) )
20 14 18 19 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) ) )
21 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) )
22 fvco3 ⊢ ( ( − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑋 ) ) → ( ( 𝑁 ∘ − ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
23 11 21 22 syl2an ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ∘ − ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
24 df-ov ⊢ ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( ( 𝑁 ∘ − ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
25 df-ov ⊢ ( 𝑥 − 𝑦 ) = ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ )
26 25 fveq2i ⊢ ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) = ( 𝑁 ‘ ( − ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
27 23 24 26 3eqtr4g ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) )
28 ovres ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
29 28 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) = ( 𝑥 𝐷 𝑦 ) )
30 27 29 eqeq12d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) ↔ ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) = ( 𝑥 𝐷 𝑦 ) ) )
31 eqcom ⊢ ( ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) = ( 𝑥 𝐷 𝑦 ) ↔ ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) )
32 30 31 bitrdi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) ↔ ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
33 32 2ralbidva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( 𝑁 ∘ − ) 𝑦 ) = ( 𝑥 ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
34 20 33 bitrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
35 34 pm5.32i ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
36 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) )
37 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
38 35 36 37 3bitr4i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )
39 6 38 bitri ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ) )