Metamath Proof Explorer

Theorem ip0r

Description: Inner product with a zero second argument. (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 ip0r 
|- ( ( W e. PreHil /\ A e. V ) -> ( A ., .0. ) = 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 1 2 3 4 5 ip0l 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( .0. ., A ) = Z )
7 6 fveq2d 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( ( *r ` F ) ` ( .0. ., A ) ) = ( ( *r ` F ) ` Z ) )
8 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
9 8 adantr 
 |-  ( ( W e. PreHil /\ A e. V ) -> W e. LMod )
10 3 5 lmod0vcl 
 |-  ( W e. LMod -> .0. e. V )
11 9 10 syl 
 |-  ( ( W e. PreHil /\ A e. V ) -> .0. e. V )
12 eqid 
 |-  ( *r ` F ) = ( *r ` F )
13 1 2 3 12 ipcj 
 |-  ( ( W e. PreHil /\ .0. e. V /\ A e. V ) -> ( ( *r ` F ) ` ( .0. ., A ) ) = ( A ., .0. ) )
14 13 3expa 
 |-  ( ( ( W e. PreHil /\ .0. e. V ) /\ A e. V ) -> ( ( *r ` F ) ` ( .0. ., A ) ) = ( A ., .0. ) )
15 14 an32s 
 |-  ( ( ( W e. PreHil /\ A e. V ) /\ .0. e. V ) -> ( ( *r ` F ) ` ( .0. ., A ) ) = ( A ., .0. ) )
16 11 15 mpdan 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( ( *r ` F ) ` ( .0. ., A ) ) = ( A ., .0. ) )
17 1 phlsrng 
 |-  ( W e. PreHil -> F e. *Ring )
18 17 adantr 
 |-  ( ( W e. PreHil /\ A e. V ) -> F e. *Ring )
19 12 4 srng0 
 |-  ( F e. *Ring -> ( ( *r ` F ) ` Z ) = Z )
20 18 19 syl 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( ( *r ` F ) ` Z ) = Z )
21 7 16 20 3eqtr3d 
 |-  ( ( W e. PreHil /\ A e. V ) -> ( A ., .0. ) = Z )