Metamath Proof Explorer

Theorem cphnmf

Description: The norm of a vector is a member of the scalar field in a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 9-Oct-2015)

Ref Expression
Hypotheses nmsq.v 
|- V = ( Base ` W )
nmsq.h 
|- ., = ( .i ` W )
nmsq.n 
|- N = ( norm ` W )
cphnmcl.f 
|- F = ( Scalar ` W )
cphnmcl.k 
|- K = ( Base ` F )
Assertion cphnmf 
|- ( W e. CPreHil -> N : V --> K )

Proof

Step Hyp Ref Expression
1 nmsq.v 
 |-  V = ( Base ` W )
2 nmsq.h 
 |-  ., = ( .i ` W )
3 nmsq.n 
 |-  N = ( norm ` W )
4 cphnmcl.f 
 |-  F = ( Scalar ` W )
5 cphnmcl.k 
 |-  K = ( Base ` F )
6 1 2 3 cphnmfval 
 |-  ( W e. CPreHil -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) )
7 simpl 
 |-  ( ( W e. CPreHil /\ x e. V ) -> W e. CPreHil )
8 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
9 8 adantr 
 |-  ( ( W e. CPreHil /\ x e. V ) -> W e. PreHil )
10 simpr 
 |-  ( ( W e. CPreHil /\ x e. V ) -> x e. V )
11 4 2 1 5 ipcl 
 |-  ( ( W e. PreHil /\ x e. V /\ x e. V ) -> ( x ., x ) e. K )
12 9 10 10 11 syl3anc 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( x ., x ) e. K )
13 1 2 3 nmsq 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( ( N ` x ) ^ 2 ) = ( x ., x ) )
14 cphngp 
 |-  ( W e. CPreHil -> W e. NrmGrp )
15 1 3 nmcl 
 |-  ( ( W e. NrmGrp /\ x e. V ) -> ( N ` x ) e. RR )
16 14 15 sylan 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( N ` x ) e. RR )
17 16 resqcld 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( ( N ` x ) ^ 2 ) e. RR )
18 13 17 eqeltrrd 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( x ., x ) e. RR )
19 16 sqge0d 
 |-  ( ( W e. CPreHil /\ x e. V ) -> 0 <_ ( ( N ` x ) ^ 2 ) )
20 19 13 breqtrd 
 |-  ( ( W e. CPreHil /\ x e. V ) -> 0 <_ ( x ., x ) )
21 4 5 cphsqrtcl 
 |-  ( ( W e. CPreHil /\ ( ( x ., x ) e. K /\ ( x ., x ) e. RR /\ 0 <_ ( x ., x ) ) ) -> ( sqrt ` ( x ., x ) ) e. K )
22 7 12 18 20 21 syl13anc 
 |-  ( ( W e. CPreHil /\ x e. V ) -> ( sqrt ` ( x ., x ) ) e. K )
23 6 22 fmpt3d 
 |-  ( W e. CPreHil -> N : V --> K )