This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )