Theorem cphngp 25229

Description: A subcomplex pre-Hilbert space is a normed group. (Contributed by Mario Carneiro, 13-Oct-2015.)

Assertion

Ref	Expression
cphngp	⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)

Proof of Theorem cphngp

Step	Hyp	Ref	Expression
1		cphnlm 25228	. 2 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
2		nlmngp 24720	. 2 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)

Syntax hints:   → wi 4   ∈ wcel 2107  NrmGrpcngp 24612  NrmModcnlm 24615  ℂPreHilccph 25222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5313

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rab 3435  df-v 3481  df-sbc 3793  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-nul 4341  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5696  df-cnv 5698  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-iota 6519  df-fv 6574  df-ov 7438  df-nlm 24621  df-cph 25224

This theorem is referenced by:  cphnmf  25251  reipcl  25253  ipge0  25254  cphpyth  25272  cphipval2  25297  4cphipval2  25298  cphipval  25299  ipcn  25302  cnmpt1ip  25303  cnmpt2ip  25304  clsocv  25306  minveclem1  25480  minveclem2  25482  minveclem3b  25484  minveclem3  25485  minveclem4a  25486  minveclem4  25488  minveclem6  25490  minveclem7  25491  pjthlem1  25493  rrxngp  46252