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