Theorem cphngp 24325

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

Syntax hints:   → wi 4   ∈ wcel 2106  NrmGrpcngp 23721  NrmModcnlm 23724  ℂPreHilccph 24318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5229

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3432  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5158  df-xp 5591  df-cnv 5593  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6385  df-fv 6435  df-ov 7271  df-nlm 23730  df-cph 24320

This theorem is referenced by:  cphnmf  24347  reipcl  24349  ipge0  24350  cphpyth  24368  cphipval2  24393  4cphipval2  24394  cphipval  24395  ipcn  24398  cnmpt1ip  24399  cnmpt2ip  24400  clsocv  24402  minveclem1  24576  minveclem2  24578  minveclem3b  24580  minveclem3  24581  minveclem4a  24582  minveclem4  24584  minveclem6  24586  minveclem7  24587  pjthlem1  24589  rrxngp  43785