Theorem cphngp 25140

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

Syntax hints:   → wi 4   ∈ wcel 2114  NrmGrpcngp 24542  NrmModcnlm 24545  ℂPreHilccph 25133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fv 6506  df-ov 7370  df-nlm 24551  df-cph 25135

This theorem is referenced by:  cphnmf  25162  reipcl  25164  ipge0  25165  cphpyth  25183  cphipval2  25208  4cphipval2  25209  cphipval  25210  ipcn  25213  cnmpt1ip  25214  cnmpt2ip  25215  clsocv  25217  minveclem1  25391  minveclem2  25393  minveclem3b  25395  minveclem3  25396  minveclem4a  25397  minveclem4  25399  minveclem6  25401  minveclem7  25402  pjthlem1  25404  rrxngp  46713