Theorem cphngp 22200

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

Step	Hyp	Ref	Expression
1		cphnlm 22199	. 2 |- ( W e. CPreHil -> W e. NrmMod )
2		nlmngp 21729	. 2 |- ( W e. NrmMod -> W e. NrmGrp )
3	1, 2	syl 17	1 |- ( W e. CPreHil -> W e. NrmGrp )

Syntax hints:   -> wi 4   e. wcel 1898  NrmGrpcngp 21641  NrmModcnlm 21644   CPreHilccph 22193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-nul 4548

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fv 5609  df-ov 6318  df-nlm 21650  df-cph 22195

This theorem is referenced by:  cphnmf  22222  reipcl  22224  ipge0  22225  ipcn  22266  cnmpt1ip  22267  cnmpt2ip  22268  clsocv  22270  minveclem1  22415  minveclem2  22417  minveclem3b  22419  minveclem3  22420  minveclem4a  22421  minveclem4  22423  minveclem6  22425  minveclem7  22426  minveclem2OLD  22429  minveclem3bOLD  22431  minveclem3OLD  22432  minveclem4aOLD  22433  minveclem4OLD  22435  minveclem6OLD  22437  minveclem7OLD  22438  pjthlem1  22440  rrxngp  38189