Metamath Proof Explorer

Theorem ldual0v

Description: The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014)

Ref Expression
Hypotheses ldualv0.v 
|- V = ( Base ` W )
ldualv0.r 
|- R = ( Scalar ` W )
ldualv0.z 
|- .0. = ( 0g ` R )
ldualv0.d 
|- D = ( LDual ` W )
ldualv0.o 
|- O = ( 0g ` D )
ldualv0.w 
|- ( ph -> W e. LMod )
Assertion ldual0v 
|- ( ph -> O = ( V X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 ldualv0.v 
 |-  V = ( Base ` W )
2 ldualv0.r 
 |-  R = ( Scalar ` W )
3 ldualv0.z 
 |-  .0. = ( 0g ` R )
4 ldualv0.d 
 |-  D = ( LDual ` W )
5 ldualv0.o 
 |-  O = ( 0g ` D )
6 ldualv0.w 
 |-  ( ph -> W e. LMod )
7 eqid 
 |-  ( LFnl ` W ) = ( LFnl ` W )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 eqid 
 |-  ( +g ` D ) = ( +g ` D )
10 2 3 1 7 lfl0f 
 |-  ( W e. LMod -> ( V X. { .0. } ) e. ( LFnl ` W ) )
11 6 10 syl 
 |-  ( ph -> ( V X. { .0. } ) e. ( LFnl ` W ) )
12 7 2 8 4 9 6 11 11 ldualvadd 
 |-  ( ph -> ( ( V X. { .0. } ) ( +g ` D ) ( V X. { .0. } ) ) = ( ( V X. { .0. } ) oF ( +g ` R ) ( V X. { .0. } ) ) )
13 1 2 8 3 7 6 11 lfladd0l 
 |-  ( ph -> ( ( V X. { .0. } ) oF ( +g ` R ) ( V X. { .0. } ) ) = ( V X. { .0. } ) )
14 12 13 eqtrd 
 |-  ( ph -> ( ( V X. { .0. } ) ( +g ` D ) ( V X. { .0. } ) ) = ( V X. { .0. } ) )
15 4 6 ldualgrp 
 |-  ( ph -> D e. Grp )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 7 4 16 6 11 ldualelvbase 
 |-  ( ph -> ( V X. { .0. } ) e. ( Base ` D ) )
18 16 9 5 grpid 
 |-  ( ( D e. Grp /\ ( V X. { .0. } ) e. ( Base ` D ) ) -> ( ( ( V X. { .0. } ) ( +g ` D ) ( V X. { .0. } ) ) = ( V X. { .0. } ) <-> O = ( V X. { .0. } ) ) )
19 15 17 18 syl2anc 
 |-  ( ph -> ( ( ( V X. { .0. } ) ( +g ` D ) ( V X. { .0. } ) ) = ( V X. { .0. } ) <-> O = ( V X. { .0. } ) ) )
20 14 19 mpbid 
 |-  ( ph -> O = ( V X. { .0. } ) )