| Step | Hyp | Ref
| Expression |
| 1 | | ngpgrp 24612 |
. . . . 5
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ Grp) |
| 2 | | tngngp2.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 3 | 2 | fvexi 6920 |
. . . . . . 7
⊢ 𝑋 ∈ V |
| 4 | | reex 11246 |
. . . . . . 7
⊢ ℝ
∈ V |
| 5 | | fex2 7958 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑋 ∈ V ∧ ℝ ∈ V) →
𝑁 ∈
V) |
| 6 | 3, 4, 5 | mp3an23 1455 |
. . . . . 6
⊢ (𝑁:𝑋⟶ℝ → 𝑁 ∈ V) |
| 7 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝐺)) |
| 8 | | tngngp2.t |
. . . . . . . 8
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) |
| 9 | 8, 2 | tngbas 24655 |
. . . . . . 7
⊢ (𝑁 ∈ V → 𝑋 = (Base‘𝑇)) |
| 10 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 11 | 8, 10 | tngplusg 24657 |
. . . . . . . 8
⊢ (𝑁 ∈ V →
(+g‘𝐺) =
(+g‘𝑇)) |
| 12 | 11 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝑁 ∈ V ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝑇)𝑦)) |
| 13 | 7, 9, 12 | grppropd 18969 |
. . . . . 6
⊢ (𝑁 ∈ V → (𝐺 ∈ Grp ↔ 𝑇 ∈ Grp)) |
| 14 | 6, 13 | syl 17 |
. . . . 5
⊢ (𝑁:𝑋⟶ℝ → (𝐺 ∈ Grp ↔ 𝑇 ∈ Grp)) |
| 15 | 1, 14 | imbitrrid 246 |
. . . 4
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp → 𝐺 ∈ Grp)) |
| 16 | 15 | imp 406 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐺 ∈ Grp) |
| 17 | | ngpms 24613 |
. . . . . 6
⊢ (𝑇 ∈ NrmGrp → 𝑇 ∈ MetSp) |
| 18 | 17 | adantl 481 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑇 ∈ MetSp) |
| 19 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑇) =
(Base‘𝑇) |
| 20 | | tngngp2.d |
. . . . . 6
⊢ 𝐷 = (dist‘𝑇) |
| 21 | 19, 20 | msmet2 24470 |
. . . . 5
⊢ (𝑇 ∈ MetSp → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(Met‘(Base‘𝑇))) |
| 22 | 18, 21 | syl 17 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (Met‘(Base‘𝑇))) |
| 23 | | eqid 2737 |
. . . . . . . . . 10
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 24 | 2, 23 | grpsubf 19037 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
| 25 | 16, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) →
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) |
| 26 | | fco 6760 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧
(-g‘𝐺):(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ) |
| 27 | 25, 26 | syldan 591 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ) |
| 28 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑁 ∈ V) |
| 29 | 8, 23 | tngds 24668 |
. . . . . . . . . 10
⊢ (𝑁 ∈ V → (𝑁 ∘
(-g‘𝐺)) =
(dist‘𝑇)) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑁 ∘ (-g‘𝐺)) = (dist‘𝑇)) |
| 31 | 20, 30 | eqtr4id 2796 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 = (𝑁 ∘ (-g‘𝐺))) |
| 32 | 31 | feq1d 6720 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷:(𝑋 × 𝑋)⟶ℝ ↔ (𝑁 ∘ (-g‘𝐺)):(𝑋 × 𝑋)⟶ℝ)) |
| 33 | 27, 32 | mpbird 257 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
| 34 | | ffn 6736 |
. . . . . 6
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ → 𝐷 Fn (𝑋 × 𝑋)) |
| 35 | | fnresdm 6687 |
. . . . . 6
⊢ (𝐷 Fn (𝑋 × 𝑋) → (𝐷 ↾ (𝑋 × 𝑋)) = 𝐷) |
| 36 | 33, 34, 35 | 3syl 18 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ (𝑋 × 𝑋)) = 𝐷) |
| 37 | 28, 9 | syl 17 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝑋 = (Base‘𝑇)) |
| 38 | 37 | sqxpeqd 5717 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝑋 × 𝑋) = ((Base‘𝑇) × (Base‘𝑇))) |
| 39 | 38 | reseq2d 5997 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
| 40 | 36, 39 | eqtr3d 2779 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 = (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) |
| 41 | 37 | fveq2d 6910 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (Met‘𝑋) = (Met‘(Base‘𝑇))) |
| 42 | 22, 40, 41 | 3eltr4d 2856 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → 𝐷 ∈ (Met‘𝑋)) |
| 43 | 16, 42 | jca 511 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝑇 ∈ NrmGrp) → (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) |
| 44 | 14 | biimpa 476 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ 𝐺 ∈ Grp) → 𝑇 ∈ Grp) |
| 45 | 44 | adantrr 717 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ Grp) |
| 46 | | simprr 773 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐷 ∈ (Met‘𝑋)) |
| 47 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁 ∈ V) |
| 48 | 47, 9 | syl 17 |
. . . . . . . 8
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑋 = (Base‘𝑇)) |
| 49 | 48 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (Met‘𝑋) = (Met‘(Base‘𝑇))) |
| 50 | 46, 49 | eleqtrd 2843 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐷 ∈ (Met‘(Base‘𝑇))) |
| 51 | | metf 24340 |
. . . . . 6
⊢ (𝐷 ∈
(Met‘(Base‘𝑇))
→ 𝐷:((Base‘𝑇) × (Base‘𝑇))⟶ℝ) |
| 52 | | ffn 6736 |
. . . . . 6
⊢ (𝐷:((Base‘𝑇) × (Base‘𝑇))⟶ℝ → 𝐷 Fn ((Base‘𝑇) × (Base‘𝑇))) |
| 53 | | fnresdm 6687 |
. . . . . 6
⊢ (𝐷 Fn ((Base‘𝑇) × (Base‘𝑇)) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = 𝐷) |
| 54 | 50, 51, 52, 53 | 4syl 19 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = 𝐷) |
| 55 | 54, 50 | eqeltrd 2841 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈ (Met‘(Base‘𝑇))) |
| 56 | 54 | fveq2d 6910 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (MetOpen‘(𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇)))) = (MetOpen‘𝐷)) |
| 57 | | simprl 771 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝐺 ∈ Grp) |
| 58 | | eqid 2737 |
. . . . . . 7
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 59 | 8, 20, 58 | tngtopn 24671 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ V) →
(MetOpen‘𝐷) =
(TopOpen‘𝑇)) |
| 60 | 57, 47, 59 | syl2anc 584 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (MetOpen‘𝐷) = (TopOpen‘𝑇)) |
| 61 | 56, 60 | eqtr2d 2778 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (TopOpen‘𝑇) = (MetOpen‘(𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))))) |
| 62 | | eqid 2737 |
. . . . 5
⊢
(TopOpen‘𝑇) =
(TopOpen‘𝑇) |
| 63 | 20 | reseq1i 5993 |
. . . . 5
⊢ (𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) = ((dist‘𝑇) ↾ ((Base‘𝑇) × (Base‘𝑇))) |
| 64 | 62, 19, 63 | isms2 24460 |
. . . 4
⊢ (𝑇 ∈ MetSp ↔ ((𝐷 ↾ ((Base‘𝑇) × (Base‘𝑇))) ∈
(Met‘(Base‘𝑇))
∧ (TopOpen‘𝑇) =
(MetOpen‘(𝐷 ↾
((Base‘𝑇) ×
(Base‘𝑇)))))) |
| 65 | 55, 61, 64 | sylanbrc 583 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ MetSp) |
| 66 | | simpl 482 |
. . . . . . 7
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁:𝑋⟶ℝ) |
| 67 | 8, 2, 4 | tngnm 24672 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑁:𝑋⟶ℝ) → 𝑁 = (norm‘𝑇)) |
| 68 | 57, 66, 67 | syl2anc 584 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑁 = (norm‘𝑇)) |
| 69 | 7, 9 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝑁 ∈ V →
(Base‘𝐺) =
(Base‘𝑇)) |
| 70 | 69, 11 | grpsubpropd 19063 |
. . . . . . 7
⊢ (𝑁 ∈ V →
(-g‘𝐺) =
(-g‘𝑇)) |
| 71 | 47, 70 | syl 17 |
. . . . . 6
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (-g‘𝐺) = (-g‘𝑇)) |
| 72 | 68, 71 | coeq12d 5875 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝑁 ∘ (-g‘𝐺)) = ((norm‘𝑇) ∘
(-g‘𝑇))) |
| 73 | 47, 29 | syl 17 |
. . . . 5
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → (𝑁 ∘ (-g‘𝐺)) = (dist‘𝑇)) |
| 74 | 72, 73 | eqtr3d 2779 |
. . . 4
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → ((norm‘𝑇) ∘ (-g‘𝑇)) = (dist‘𝑇)) |
| 75 | | eqimss 4042 |
. . . 4
⊢
(((norm‘𝑇)
∘ (-g‘𝑇)) = (dist‘𝑇) → ((norm‘𝑇) ∘ (-g‘𝑇)) ⊆ (dist‘𝑇)) |
| 76 | 74, 75 | syl 17 |
. . 3
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → ((norm‘𝑇) ∘ (-g‘𝑇)) ⊆ (dist‘𝑇)) |
| 77 | | eqid 2737 |
. . . 4
⊢
(norm‘𝑇) =
(norm‘𝑇) |
| 78 | | eqid 2737 |
. . . 4
⊢
(-g‘𝑇) = (-g‘𝑇) |
| 79 | | eqid 2737 |
. . . 4
⊢
(dist‘𝑇) =
(dist‘𝑇) |
| 80 | 77, 78, 79 | isngp 24609 |
. . 3
⊢ (𝑇 ∈ NrmGrp ↔ (𝑇 ∈ Grp ∧ 𝑇 ∈ MetSp ∧
((norm‘𝑇) ∘
(-g‘𝑇))
⊆ (dist‘𝑇))) |
| 81 | 45, 65, 76, 80 | syl3anbrc 1344 |
. 2
⊢ ((𝑁:𝑋⟶ℝ ∧ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋))) → 𝑇 ∈ NrmGrp) |
| 82 | 43, 81 | impbida 801 |
1
⊢ (𝑁:𝑋⟶ℝ → (𝑇 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐷 ∈ (Met‘𝑋)))) |