Metamath Proof Explorer

Theorem cphipcl

Description: An inner product is a member of the complex numbers. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses nmsq.v 
|- V = ( Base ` W )
nmsq.h 
|- ., = ( .i ` W )
Assertion cphipcl 
|- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )

Proof

Step Hyp Ref Expression
1 nmsq.v 
 |-  V = ( Base ` W )
2 nmsq.h 
 |-  ., = ( .i ` W )
3 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
4 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
5 3 4 cphsubrg 
 |-  ( W e. CPreHil -> ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) )
6 cnfldbas 
 |-  CC = ( Base ` CCfld )
7 6 subrgss 
 |-  ( ( Base ` ( Scalar ` W ) ) e. ( SubRing ` CCfld ) -> ( Base ` ( Scalar ` W ) ) C_ CC )
8 5 7 syl 
 |-  ( W e. CPreHil -> ( Base ` ( Scalar ` W ) ) C_ CC )
9 8 3ad2ant1 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( Base ` ( Scalar ` W ) ) C_ CC )
10 cphphl 
 |-  ( W e. CPreHil -> W e. PreHil )
11 3 2 1 4 ipcl 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. ( Base ` ( Scalar ` W ) ) )
12 10 11 syl3an1 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. ( Base ` ( Scalar ` W ) ) )
13 9 12 sseldd 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. CC )