MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cphngp Unicode version

Theorem cphngp 18662
Description: A complex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)
Assertion
Ref Expression
cphngp  |-  ( W  e.  CPreHil  ->  W  e. NrmGrp )

Proof of Theorem cphngp
StepHypRef Expression
1 cphnlm 18661 . 2  |-  ( W  e.  CPreHil  ->  W  e. NrmMod )
2 nlmngp 18240 . 2  |-  ( W  e. NrmMod  ->  W  e. NrmGrp )
31, 2syl 15 1  |-  ( W  e.  CPreHil  ->  W  e. NrmGrp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701  NrmGrpcngp 18152  NrmModcnlm 18155   CPreHilccph 18655
This theorem is referenced by:  cphnmf  18684  reipcl  18686  ipge0  18687  ipcn  18726  cnmpt1ip  18727  cnmpt2ip  18728  clsocv  18730  minveclem1  18841  minveclem2  18843  minveclem3b  18845  minveclem3  18846  minveclem4a  18847  minveclem4  18849  minveclem6  18851  minveclem7  18852  pjthlem1  18854
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-nul 4186
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-xp 4732  df-cnv 4734  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fv 5300  df-ov 5903  df-nlm 18161  df-cph 18657
  Copyright terms: Public domain W3C validator