Metamath Proof Explorer

Theorem lcd0vvalN

Description: Value of the zero functional at any vector. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lcd0vval.h 
|- H = ( LHyp ` K )
lcd0vval.u 
|- U = ( ( DVecH ` K ) ` W )
lcd0vval.v 
|- V = ( Base ` U )
lcd0vval.s 
|- S = ( Scalar ` U )
lcd0vval.z 
|- .0. = ( 0g ` S )
lcd0vval.c 
|- C = ( ( LCDual ` K ) ` W )
lcd0vval.o 
|- O = ( 0g ` C )
lcd0vval.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcd0vval.x 
|- ( ph -> X e. V )
Assertion lcd0vvalN 
|- ( ph -> ( O ` X ) = .0. )

Proof

Step Hyp Ref Expression
1 lcd0vval.h 
 |-  H = ( LHyp ` K )
2 lcd0vval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcd0vval.v 
 |-  V = ( Base ` U )
4 lcd0vval.s 
 |-  S = ( Scalar ` U )
5 lcd0vval.z 
 |-  .0. = ( 0g ` S )
6 lcd0vval.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 lcd0vval.o 
 |-  O = ( 0g ` C )
8 lcd0vval.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 lcd0vval.x 
 |-  ( ph -> X e. V )
10 1 2 3 4 5 6 7 8 lcd0v 
 |-  ( ph -> O = ( V X. { .0. } ) )
11 10 fveq1d 
 |-  ( ph -> ( O ` X ) = ( ( V X. { .0. } ) ` X ) )
12 5 fvexi 
 |-  .0. e. _V
13 12 fvconst2 
 |-  ( X e. V -> ( ( V X. { .0. } ) ` X ) = .0. )
14 9 13 syl 
 |-  ( ph -> ( ( V X. { .0. } ) ` X ) = .0. )
15 11 14 eqtrd 
 |-  ( ph -> ( O ` X ) = .0. )