Metamath Proof Explorer

Theorem cphnlm

Description: A subcomplex pre-Hilbert space is a normed module. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Assertion cphnlm 
|- ( W e. CPreHil -> W e. NrmMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` W ) = ( Base ` W )
2 eqid 
 |-  ( .i ` W ) = ( .i ` W )
3 eqid 
 |-  ( norm ` W ) = ( norm ` W )
4 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
5 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
6 1 2 3 4 5 iscph 
 |-  ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) ) /\ ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` W ) ) /\ ( norm ` W ) = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) ) )
7 6 simp1bi 
 |-  ( W e. CPreHil -> ( W e. PreHil /\ W e. NrmMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) ) )
8 7 simp2d 
 |-  ( W e. CPreHil -> W e. NrmMod )