Theorem cphngp 25303

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

Syntax hints:   → wi 4   ∈ wcel 2149  NrmGrpcngp 24705  NrmModcnlm 24708  ℂPreHilccph 25296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5273

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rab 3424  df-v 3465  df-sbc 3754  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-xp 5670  df-cnv 5672  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6495  df-fv 6547  df-ov 7416  df-nlm 24714  df-cph 25298

This theorem is referenced by:  cphnmf  25325  reipcl  25327  ipge0  25328  cphpyth  25346  cphipval2  25371  4cphipval2  25372  cphipval  25373  ipcn  25376  cnmpt1ip  25377  cnmpt2ip  25378  clsocv  25380  minveclem1  25554  minveclem2  25556  minveclem3b  25558  minveclem3  25559  minveclem4a  25560  minveclem4  25562  minveclem6  25564  minveclem7  25565  pjthlem1  25567  rrxngp  46928