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

Metamath Proof Explorer

Theorem isngp2

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 ‘ 𝐺 )
isngp2.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
isngp2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
Assertion isngp2 ( 𝐺 ∈ 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 isngp2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6 1 2 3 isngp ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
7 resss ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) ⊆ 𝐷
8 5 7 eqsstri ⊢ 𝐸 ⊆ 𝐷
9 sseq1 ⊢ ( ( 𝑁 ∘ − ) = 𝐸 → ( ( 𝑁 ∘ − ) ⊆ 𝐷 ↔ 𝐸 ⊆ 𝐷 ) )
10 8 9 mpbiri ⊢ ( ( 𝑁 ∘ − ) = 𝐸 → ( 𝑁 ∘ − ) ⊆ 𝐷 )
11 3 reseq1i ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
12 5 11 eqtri ⊢ 𝐸 = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
13 4 12 msmet ⊢ ( 𝐺 ∈ MetSp → 𝐸 ∈ ( Met ‘ 𝑋 ) )
14 1 4 3 5 nmf2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ) → 𝑁 : 𝑋 ⟶ ℝ )
15 13 14 sylan2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → 𝑁 : 𝑋 ⟶ ℝ )
16 4 2 grpsubf ⊢ ( 𝐺 ∈ Grp → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
17 16 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
18 fco ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ − : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
19 15 17 18 syl2an2r ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ )
20 19 fdmd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → dom ( 𝑁 ∘ − ) = ( 𝑋 × 𝑋 ) )
21 20 reseq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝐸 ↾ dom ( 𝑁 ∘ − ) ) = ( 𝐸 ↾ ( 𝑋 × 𝑋 ) ) )
22 4 12 msf ⊢ ( 𝐺 ∈ MetSp → 𝐸 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
23 22 ad2antlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → 𝐸 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
24 23 ffund ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → Fun 𝐸 )
25 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) ⊆ 𝐷 )
26 ssv ⊢ ℝ ⊆ V
27 fss ⊢ ( ( ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ ℝ ∧ ℝ ⊆ V ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ V )
28 19 26 27 sylancl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ V )
29 fssxp ⊢ ( ( 𝑁 ∘ − ) : ( 𝑋 × 𝑋 ) ⟶ V → ( 𝑁 ∘ − ) ⊆ ( ( 𝑋 × 𝑋 ) × V ) )
30 28 29 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) ⊆ ( ( 𝑋 × 𝑋 ) × V ) )
31 25 30 ssind ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) ⊆ ( 𝐷 ∩ ( ( 𝑋 × 𝑋 ) × V ) ) )
32 df-res ⊢ ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( 𝐷 ∩ ( ( 𝑋 × 𝑋 ) × V ) )
33 5 32 eqtri ⊢ 𝐸 = ( 𝐷 ∩ ( ( 𝑋 × 𝑋 ) × V ) )
34 31 33 sseqtrrdi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) ⊆ 𝐸 )
35 funssres ⊢ ( ( Fun 𝐸 ∧ ( 𝑁 ∘ − ) ⊆ 𝐸 ) → ( 𝐸 ↾ dom ( 𝑁 ∘ − ) ) = ( 𝑁 ∘ − ) )
36 24 34 35 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝐸 ↾ dom ( 𝑁 ∘ − ) ) = ( 𝑁 ∘ − ) )
37 ffn ⊢ ( 𝐸 : ( 𝑋 × 𝑋 ) ⟶ ℝ → 𝐸 Fn ( 𝑋 × 𝑋 ) )
38 fnresdm ⊢ ( 𝐸 Fn ( 𝑋 × 𝑋 ) → ( 𝐸 ↾ ( 𝑋 × 𝑋 ) ) = 𝐸 )
39 23 37 38 3syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝐸 ↾ ( 𝑋 × 𝑋 ) ) = 𝐸 )
40 21 36 39 3eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) → ( 𝑁 ∘ − ) = 𝐸 )
41 40 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ( 𝑁 ∘ − ) ⊆ 𝐷 → ( 𝑁 ∘ − ) = 𝐸 ) )
42 10 41 impbid2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ( 𝑁 ∘ − ) = 𝐸 ↔ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
43 42 pm5.32i ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) = 𝐸 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
44 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = 𝐸 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) = 𝐸 ) )
45 df-3an ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) ↔ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
46 43 44 45 3bitr4i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = 𝐸 ) ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) ⊆ 𝐷 ) )
47 6 46 bitr4i ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ( 𝑁 ∘ − ) = 𝐸 ) )