| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ngpgrp | Structured version Visualization version GIF version | ||
| Description: A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| Ref | Expression |
|---|---|
| ngpgrp | ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2765 | . . 3 ⊢ (norm‘𝐺) = (norm‘𝐺) | |
| 2 | eqid 2765 | . . 3 ⊢ (-g‘𝐺) = (-g‘𝐺) | |
| 3 | eqid 2765 | . . 3 ⊢ (dist‘𝐺) = (dist‘𝐺) | |
| 4 | 1, 2, 3 | isngp 24806 | . 2 ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ((norm‘𝐺) ∘ (-g‘𝐺)) ⊆ (dist‘𝐺))) |
| 5 | 4 | simp1bi 1163 | 1 ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2146 ⊆ wss 3906 ∘ ccom 5667 ‘cfv 6540 distcds 17343 Grpcgrp 19046 -gcsg 19048 MetSpcms 24528 normcnm 24786 NrmGrpcngp 24787 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-co 5672 df-iota 6496 df-fv 6548 df-ngp 24793 |
| This theorem is used by: ngpds 24814 ngpds2 24816 ngpds3 24818 ngprcan 24820 isngp4 24822 ngpinvds 24823 ngpsubcan 24824 nmf 24825 nmge0 24827 nmeq0 24828 nminv 24831 nmmtri 24832 nmsub 24833 nmrtri 24834 nm2dif 24835 nmtri 24836 nmtri2 24837 ngpi 24838 nm0 24839 ngptgp 24846 tngngp2 24862 tnggrpr 24865 nrmtngnrm 24868 nlmdsdi 24891 nlmdsdir 24892 nrginvrcnlem 24901 ngpocelbl 24914 nmo0 24945 nmotri 24949 0nghm 24951 nmoid 24952 idnghm 24953 nmods 24954 nmcn 25055 nmoleub2lem2 25328 nmhmcn 25332 cphpyth 25428 cphipval2 25453 4cphipval2 25454 cphipval 25455 ipcnlem2 25456 nglmle 25514 qqhcn 34447 |
| Copyright terms: Public domain | W3C validator |