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 ⊢ N = norm ⁡ G
isngp.z ⊢ - ˙ = - G
isngp.d ⊢ D = dist ⁡ G
isngp2.x ⊢ X = Base G
isngp2.e ⊢ E = D ↾ X × X
Assertion isngp2 ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E

Proof

Step Hyp Ref Expression
1 isngp.n ⊢ N = norm ⁡ G
2 isngp.z ⊢ - ˙ = - G
3 isngp.d ⊢ D = dist ⁡ G
4 isngp2.x ⊢ X = Base G
5 isngp2.e ⊢ E = D ↾ X × X
6 1 2 3 isngp ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
7 resss ⊢ D ↾ X × X ⊆ D
8 5 7 eqsstri ⊢ E ⊆ D
9 sseq1 ⊢ N ∘ - ˙ = E → N ∘ - ˙ ⊆ D ↔ E ⊆ D
10 8 9 mpbiri ⊢ N ∘ - ˙ = E → N ∘ - ˙ ⊆ D
11 3 reseq1i ⊢ D ↾ X × X = dist ⁡ G ↾ X × X
12 5 11 eqtri ⊢ E = dist ⁡ G ↾ X × X
13 4 12 msmet ⊢ G ∈ MetSp → E ∈ Met ⁡ X
14 1 4 3 5 nmf2 ⊢ G ∈ Grp ∧ E ∈ Met ⁡ X → N : X ⟶ ℝ
15 13 14 sylan2 ⊢ G ∈ Grp ∧ G ∈ MetSp → N : X ⟶ ℝ
16 4 2 grpsubf ⊢ G ∈ Grp → - ˙ : X × X ⟶ X
17 16 ad2antrr ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → - ˙ : X × X ⟶ X
18 fco ⊢ N : X ⟶ ℝ ∧ - ˙ : X × X ⟶ X → N ∘ - ˙ : X × X ⟶ ℝ
19 15 17 18 syl2an2r ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ : X × X ⟶ ℝ
20 19 fdmd ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → dom ⁡ N ∘ - ˙ = X × X
21 20 reseq2d ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → E ↾ dom ⁡ N ∘ - ˙ = E ↾ X × X
22 4 12 msf ⊢ G ∈ MetSp → E : X × X ⟶ ℝ
23 22 ad2antlr ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → E : X × X ⟶ ℝ
24 23 ffund ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → Fun ⁡ E
25 simpr ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ ⊆ D
26 ssv ⊢ ℝ ⊆ V
27 fss ⊢ N ∘ - ˙ : X × X ⟶ ℝ ∧ ℝ ⊆ V → N ∘ - ˙ : X × X ⟶ V
28 19 26 27 sylancl ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ : X × X ⟶ V
29 fssxp ⊢ N ∘ - ˙ : X × X ⟶ V → N ∘ - ˙ ⊆ X × X × V
30 28 29 syl ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ ⊆ X × X × V
31 25 30 ssind ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ ⊆ D ∩ X × X × V
32 df-res ⊢ D ↾ X × X = D ∩ X × X × V
33 5 32 eqtri ⊢ E = D ∩ X × X × V
34 31 33 sseqtrrdi ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ ⊆ E
35 funssres ⊢ Fun ⁡ E ∧ N ∘ - ˙ ⊆ E → E ↾ dom ⁡ N ∘ - ˙ = N ∘ - ˙
36 24 34 35 syl2anc ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → E ↾ dom ⁡ N ∘ - ˙ = N ∘ - ˙
37 ffn ⊢ E : X × X ⟶ ℝ → E Fn X × X
38 fnresdm ⊢ E Fn X × X → E ↾ X × X = E
39 23 37 38 3syl ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → E ↾ X × X = E
40 21 36 39 3eqtr3d ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D → N ∘ - ˙ = E
41 40 ex ⊢ G ∈ Grp ∧ G ∈ MetSp → N ∘ - ˙ ⊆ D → N ∘ - ˙ = E
42 10 41 impbid2 ⊢ G ∈ Grp ∧ G ∈ MetSp → N ∘ - ˙ = E ↔ N ∘ - ˙ ⊆ D
43 42 pm5.32i ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
44 df-3an ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E
45 df-3an ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
46 43 44 45 3bitr4i ⊢ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ ⊆ D
47 6 46 bitr4i ⊢ G ∈ NrmGrp ↔ G ∈ Grp ∧ G ∈ MetSp ∧ N ∘ - ˙ = E