Step | Hyp | Ref
| Expression |
1 | | ngpgrp 22213 |
. . . . 5
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ Grp) |
2 | | tngngp2.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
3 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
4 | 2, 3 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑋 ∈ V |
5 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
6 | | fex2 7014 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V) →
𝑁 ∈
V) |
7 | 4, 5, 6 | mp3an23 1408 |
. . . . . 6
⊢ (𝑁:𝑋⟶ℝ → 𝑁 ∈ V) |
8 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝐺)) |
9 | | tngngp2.t |
. . . . . . . 8
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) |
10 | 9, 2 | tngbas 22255 |
. . . . . . 7
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝑇)) |
11 | | eqid 2610 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | 9, 11 | tngplusg 22256 |
. . . . . . . 8
⊢ (𝑁 ∈ V →
(+g‘𝐺) =
(+g‘𝑇)) |
13 | 12 | oveqdr 6573 |
. . . . . . 7
⊢ ((𝑁 ∈ V ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝑇)𝑦)) |
14 | 8, 10, 13 | grppropd 17260 |
. . . . . 6
⊢ (𝑁 ∈ V → (𝐺 ∈ Grp ↔ 𝑇 ∈ Grp)) |
15 | 7, 14 | syl 17 |
. . . . 5
⊢ (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ↔ 𝑇 ∈ Grp)) |
16 | 1, 15 | syl5ibr 235 |
. . . 4
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → 𝐺 ∈ Grp)) |
17 | 16 | imp 444 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp) |
18 | | ngpms 22214 |
. . . . . 6
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp) |
19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑇 ∈ MetSp) |
20 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
21 | | tngngp2.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝑇) |
22 | 20, 21 | msmet2 22075 |
. . . . 5
⊢ (𝑇 ∈ MetSp → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(Met‘(Base‘𝑇))) |
23 | 19, 22 | syl 17 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (Met‘(Base‘𝑇))) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
25 | 2, 24 | grpsubf 17317 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
26 | 17, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
27 | | fco 5971 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ) |
28 | 26, 27 | syldan 486 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ) |
29 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑁 ∈ V) |
30 | 9, 24 | tngds 22262 |
. . . . . . . . . 10
⊢ (𝑁 ∈ V → (𝑁 ∘
(-g‘𝐺)) =
(dist‘𝑇)) |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑁 ∘ (-g‘𝐺)) = (dist‘𝑇)) |
32 | 31, 21 | syl6reqr 2663 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 = (𝑁 ∘ (-g‘𝐺))) |
33 | 32 | feq1d 5943 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷:(𝑋 × 𝑋)⟶ℝ ↔ (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ)) |
34 | 28, 33 | mpbird 246 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
35 | | ffn 5958 |
. . . . . 6
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ → 𝐷 Fn (𝑋 × 𝑋)) |
36 | | fnresdm 5914 |
. . . . . 6
⊢ (𝐷 Fn (𝑋 × 𝑋) → (𝐷 ↾ (𝑋 × 𝑋)) = 𝐷) |
37 | 34, 35, 36 | 3syl 18 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ (𝑋 × 𝑋)) = 𝐷) |
38 | 29, 10 | syl 17 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑋 = (Base‘𝑇)) |
39 | 38 | sqxpeqd 5065 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑋 × 𝑋) = ((Base‘𝑇) × (Base‘𝑇))) |
40 | 39 | reseq2d 5317 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
41 | 37, 40 | eqtr3d 2646 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 = (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
42 | 38 | fveq2d 6107 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (Met‘𝑋) = (Met‘(Base‘𝑇))) |
43 | 23, 41, 42 | 3eltr4d 2703 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 ∈ (Met‘𝑋)) |
44 | 17, 43 | jca 553 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) |
45 | 15 | biimpa 500 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝐺 ∈ Grp) → 𝑇 ∈ Grp) |
46 | 45 | adantrr 749 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ Grp) |
47 | | simprr 792 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐷 ∈ (Met‘𝑋)) |
48 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁 ∈ V) |
49 | 48, 10 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑋 = (Base‘𝑇)) |
50 | 49 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (Met‘𝑋) = (Met‘(Base‘𝑇))) |
51 | 47, 50 | eleqtrd 2690 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐷 ∈ (Met‘(Base‘𝑇))) |
52 | | metf 21945 |
. . . . . . 7
⊢ (𝐷 ∈
(Met‘(Base‘𝑇))
→ 𝐷:((Base‘𝑇) × (Base‘𝑇))⟶ℝ) |
53 | 51, 52 | syl 17 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐷:((Base‘𝑇) × (Base‘𝑇))⟶ℝ) |
54 | | ffn 5958 |
. . . . . 6
⊢ (𝐷:((Base‘𝑇) × (Base‘𝑇))⟶ℝ → 𝐷 Fn ((Base‘𝑇) × (Base‘𝑇))) |
55 | | fnresdm 5914 |
. . . . . 6
⊢ (𝐷 Fn ((Base‘𝑇) × (Base‘𝑇)) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = 𝐷) |
56 | 53, 54, 55 | 3syl 18 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = 𝐷) |
57 | 56, 51 | eqeltrd 2688 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (Met‘(Base‘𝑇))) |
58 | 56 | fveq2d 6107 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (MetOpen‘(𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘𝐷)) |
59 | | simprl 790 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐺 ∈ Grp) |
60 | | eqid 2610 |
. . . . . . 7
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
61 | 9, 21, 60 | tngtopn 22264 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ V) →
(MetOpen‘𝐷) =
(TopOpen‘𝑇)) |
62 | 59, 48, 61 | syl2anc 691 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (MetOpen‘𝐷) = (TopOpen‘𝑇)) |
63 | 58, 62 | eqtr2d 2645 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (TopOpen‘𝑇) = (MetOpen‘(𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
64 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘𝑇) =
(TopOpen‘𝑇) |
65 | 21 | reseq1i 5313 |
. . . . 5
⊢ (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) |
66 | 64, 20, 65 | isms2 22065 |
. . . 4
⊢ (𝑇 ∈ MetSp ↔ ((𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(Met‘(Base‘𝑇))
∧ (TopOpen‘𝑇) =
(MetOpen‘(𝐷 ↾
((Base‘𝑇) ×
(Base‘𝑇)))))) |
67 | 57, 63, 66 | sylanbrc 695 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ MetSp) |
68 | | simpl 472 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁:𝑋⟶ℝ) |
69 | 9, 2, 5 | tngnm 22265 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇)) |
70 | 59, 68, 69 | syl2anc 691 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁 = (norm‘𝑇)) |
71 | 8, 10 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝑁 ∈ V →
(Base‘𝐺) =
(Base‘𝑇)) |
72 | 71, 12 | grpsubpropd 17343 |
. . . . . . 7
⊢ (𝑁 ∈ V →
(-g‘𝐺) =
(-g‘𝑇)) |
73 | 48, 72 | syl 17 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (-g‘𝐺) = (-g‘𝑇)) |
74 | 70, 73 | coeq12d 5208 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝑁 ∘ (-g‘𝐺)) = ((norm‘𝑇) ∘
(-g‘𝑇))) |
75 | 48, 30 | syl 17 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝑁 ∘ (-g‘𝐺)) = (dist‘𝑇)) |
76 | 74, 75 | eqtr3d 2646 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → ((norm‘𝑇) ∘ (-g‘𝑇)) = (dist‘𝑇)) |
77 | | eqimss 3620 |
. . . 4
⊢
(((norm‘𝑇)
∘ (-g‘𝑇)) = (dist‘𝑇) → ((norm‘𝑇) ∘ (-g‘𝑇)) ⊆ (dist‘𝑇)) |
78 | 76, 77 | syl 17 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → ((norm‘𝑇) ∘ (-g‘𝑇)) ⊆ (dist‘𝑇)) |
79 | | eqid 2610 |
. . . 4
⊢
(norm‘𝑇) =
(norm‘𝑇) |
80 | | eqid 2610 |
. . . 4
⊢
(-g‘𝑇) = (-g‘𝑇) |
81 | | eqid 2610 |
. . . 4
⊢
(dist‘𝑇) =
(dist‘𝑇) |
82 | 79, 80, 81 | isngp 22210 |
. . 3
⊢ (𝑇 ∈ NrmGrp ↔ (𝑇 ∈ Grp ∧ 𝑇 ∈ MetSp ∧
((norm‘𝑇) ∘
(-g‘𝑇))
⊆ (dist‘𝑇))) |
83 | 46, 67, 78, 82 | syl3anbrc 1239 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ NrmGrp) |
84 | 44, 83 | impbida 873 |
1
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋)))) |