Theorem cphngp 25080

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 25079	. 2 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod)
2		nlmngp 24571	. 2 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
3	1, 2	syl 17	1 ⊢ (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)

Syntax hints:   → wi 4   ∈ wcel 2109  NrmGrpcngp 24471  NrmModcnlm 24474  ℂPreHilccph 25073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5269

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2928  df-ral 3047  df-rab 3412  df-v 3457  df-sbc 3762  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-nul 4305  df-if 4497  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-br 5116  df-opab 5178  df-mpt 5197  df-xp 5652  df-cnv 5654  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-iota 6472  df-fv 6527  df-ov 7397  df-nlm 24480  df-cph 25075

This theorem is referenced by:  cphnmf  25102  reipcl  25104  ipge0  25105  cphpyth  25123  cphipval2  25148  4cphipval2  25149  cphipval  25150  ipcn  25153  cnmpt1ip  25154  cnmpt2ip  25155  clsocv  25157  minveclem1  25331  minveclem2  25333  minveclem3b  25335  minveclem3  25336  minveclem4a  25337  minveclem4  25339  minveclem6  25341  minveclem7  25342  pjthlem1  25344  rrxngp  46256