Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β wcel 2107
β wss 3914 β
ccom 5641 βcfv 6500
distcds 17150 Grpcgrp 18756
-gcsg 18758
MetSpcms 23694 normcnm 23955
NrmGrpcngp 23956 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-co 5646 df-iota 6452 df-fv 6508 df-ngp 23962 |
This theorem is referenced by: ngpxms
23980 ngptps
23981 ngpmet
23982 isngp4
23991 nmmtri
24001 nmrtri
24003 subgngp
24014 ngptgp
24015 tngngp2
24039 nlmvscnlem2
24072 nlmvscnlem1
24073 nlmvscn
24074 nrginvrcn
24079 nghmcn
24132 nmcn
24230 nmhmcn
24506 ipcnlem2
24631 ipcnlem1
24632 ipcn
24633 nglmle
24689 cssbn
24762 minveclem2
24813 minveclem3b
24815 minveclem3
24816 minveclem4
24819 minveclem7
24822 |