Theorem ip0l

Description: Inner product with a zero first argument. Part of proof of Theorem 6.44 of Ponnusamy p. 361. (Contributed by NM, 5-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	|- F = ( Scalar ` W )
	phllmhm.h	|- ., = ( .i ` W )
	phllmhm.v	|- V = ( Base ` W )
	ip0l.z	|- Z = ( 0g ` F )
	ip0l.o	|- .0. = ( 0g ` W )
Assertion	ip0l	|- ( ( W e. PreHil /\ A e. V ) -> ( .0. ., A ) = Z )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	|- F = ( Scalar ` W )
2		phllmhm.h	|- ., = ( .i ` W )
3		phllmhm.v	|- V = ( Base ` W )
4		ip0l.z	|- Z = ( 0g ` F )
5		ip0l.o	|- .0. = ( 0g ` W )
6		phllmod	|- ( W e. PreHil -> W e. LMod )
7		lmodgrp	|- ( W e. LMod -> W e. Grp )
8	3 5	grpidcl	|- ( W e. Grp -> .0. e. V )
9	6 7 8	3syl	|- ( W e. PreHil -> .0. e. V )
10	9	adantr	|- ( ( W e. PreHil /\ A e. V ) -> .0. e. V )
11		oveq1	|- ( x = .0. -> ( x ., A ) = ( .0. ., A ) )
12		eqid	|- ( x e. V |-> ( x ., A ) ) = ( x e. V |-> ( x ., A ) )
13		ovex	|- ( .0. ., A ) e. _V
14	11 12 13	fvmpt	|- ( .0. e. V -> ( ( x e. V |-> ( x ., A ) ) ` .0. ) = ( .0. ., A ) )
15	10 14	syl	|- ( ( W e. PreHil /\ A e. V ) -> ( ( x e. V |-> ( x ., A ) ) ` .0. ) = ( .0. ., A ) )
16	1 2 3 12	phllmhm	|- ( ( W e. PreHil /\ A e. V ) -> ( x e. V |-> ( x ., A ) ) e. ( W LMHom ( ringLMod ` F ) ) )
17		lmghm	|- ( ( x e. V |-> ( x ., A ) ) e. ( W LMHom ( ringLMod ` F ) ) -> ( x e. V |-> ( x ., A ) ) e. ( W GrpHom ( ringLMod ` F ) ) )
18		rlm0	|- ( 0g ` F ) = ( 0g ` ( ringLMod ` F ) )
19	4 18	eqtri	|- Z = ( 0g ` ( ringLMod ` F ) )
20	5 19	ghmid	|- ( ( x e. V |-> ( x ., A ) ) e. ( W GrpHom ( ringLMod ` F ) ) -> ( ( x e. V |-> ( x ., A ) ) ` .0. ) = Z )
21	16 17 20	3syl	|- ( ( W e. PreHil /\ A e. V ) -> ( ( x e. V |-> ( x ., A ) ) ` .0. ) = Z )
22	15 21	eqtr3d	|- ( ( W e. PreHil /\ A e. V ) -> ( .0. ., A ) = Z )