Metamath Proof Explorer


Theorem phllmhm

Description: The inner product of a pre-Hilbert space is linear in its left argument. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f
|- F = ( Scalar ` W )
phllmhm.h
|- ., = ( .i ` W )
phllmhm.v
|- V = ( Base ` W )
phllmhm.g
|- G = ( x e. V |-> ( x ., A ) )
Assertion phllmhm
|- ( ( W e. PreHil /\ A e. V ) -> G e. ( W LMHom ( ringLMod ` F ) ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f
 |-  F = ( Scalar ` W )
2 phllmhm.h
 |-  ., = ( .i ` W )
3 phllmhm.v
 |-  V = ( Base ` W )
4 phllmhm.g
 |-  G = ( x e. V |-> ( x ., A ) )
5 eqid
 |-  ( 0g ` W ) = ( 0g ` W )
6 eqid
 |-  ( *r ` F ) = ( *r ` F )
7 eqid
 |-  ( 0g ` F ) = ( 0g ` F )
8 3 1 2 5 6 7 isphl
 |-  ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. y e. V ( ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( y ., y ) = ( 0g ` F ) -> y = ( 0g ` W ) ) /\ A. x e. V ( ( *r ` F ) ` ( y ., x ) ) = ( x ., y ) ) ) )
9 8 simp3bi
 |-  ( W e. PreHil -> A. y e. V ( ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( y ., y ) = ( 0g ` F ) -> y = ( 0g ` W ) ) /\ A. x e. V ( ( *r ` F ) ` ( y ., x ) ) = ( x ., y ) ) )
10 simp1
 |-  ( ( ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( y ., y ) = ( 0g ` F ) -> y = ( 0g ` W ) ) /\ A. x e. V ( ( *r ` F ) ` ( y ., x ) ) = ( x ., y ) ) -> ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) )
11 10 ralimi
 |-  ( A. y e. V ( ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( y ., y ) = ( 0g ` F ) -> y = ( 0g ` W ) ) /\ A. x e. V ( ( *r ` F ) ` ( y ., x ) ) = ( x ., y ) ) -> A. y e. V ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) )
12 9 11 syl
 |-  ( W e. PreHil -> A. y e. V ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) )
13 oveq2
 |-  ( y = A -> ( x ., y ) = ( x ., A ) )
14 13 mpteq2dv
 |-  ( y = A -> ( x e. V |-> ( x ., y ) ) = ( x e. V |-> ( x ., A ) ) )
15 14 4 eqtr4di
 |-  ( y = A -> ( x e. V |-> ( x ., y ) ) = G )
16 15 eleq1d
 |-  ( y = A -> ( ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) <-> G e. ( W LMHom ( ringLMod ` F ) ) ) )
17 16 rspccva
 |-  ( ( A. y e. V ( x e. V |-> ( x ., y ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ A e. V ) -> G e. ( W LMHom ( ringLMod ` F ) ) )
18 12 17 sylan
 |-  ( ( W e. PreHil /\ A e. V ) -> G e. ( W LMHom ( ringLMod ` F ) ) )