Metamath Proof Explorer

Theorem ipcl

Description: Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ipcl.f 
|- K = ( Base ` F )
Assertion ipcl 
|- ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. K )

Proof

Step Hyp Ref Expression
1 phlsrng.f 
 |-  F = ( Scalar ` W )
2 phllmhm.h 
 |-  ., = ( .i ` W )
3 phllmhm.v 
 |-  V = ( Base ` W )
4 ipcl.f 
 |-  K = ( Base ` F )
5 eqid 
 |-  ( x e. V |-> ( x ., B ) ) = ( x e. V |-> ( x ., B ) )
6 1 2 3 5 phllmhm 
 |-  ( ( W e. PreHil /\ B e. V ) -> ( x e. V |-> ( x ., B ) ) e. ( W LMHom ( ringLMod ` F ) ) )
7 rlmbas 
 |-  ( Base ` F ) = ( Base ` ( ringLMod ` F ) )
8 4 7 eqtri 
 |-  K = ( Base ` ( ringLMod ` F ) )
9 3 8 lmhmf 
 |-  ( ( x e. V |-> ( x ., B ) ) e. ( W LMHom ( ringLMod ` F ) ) -> ( x e. V |-> ( x ., B ) ) : V --> K )
10 6 9 syl 
 |-  ( ( W e. PreHil /\ B e. V ) -> ( x e. V |-> ( x ., B ) ) : V --> K )
11 5 fmpt 
 |-  ( A. x e. V ( x ., B ) e. K <-> ( x e. V |-> ( x ., B ) ) : V --> K )
12 10 11 sylibr 
 |-  ( ( W e. PreHil /\ B e. V ) -> A. x e. V ( x ., B ) e. K )
13 oveq1 
 |-  ( x = A -> ( x ., B ) = ( A ., B ) )
14 13 eleq1d 
 |-  ( x = A -> ( ( x ., B ) e. K <-> ( A ., B ) e. K ) )
15 14 rspccva 
 |-  ( ( A. x e. V ( x ., B ) e. K /\ A e. V ) -> ( A ., B ) e. K )
16 12 15 stoic3 
 |-  ( ( W e. PreHil /\ B e. V /\ A e. V ) -> ( A ., B ) e. K )
17 16 3com23 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A ., B ) e. K )