This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lkr0f2

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015)

Ref Expression
Hypotheses lkr0f2.v 
|- V = ( Base ` W )
lkr0f2.f 
|- F = ( LFnl ` W )
lkr0f2.k 
|- K = ( LKer ` W )
lkr0f2.d 
|- D = ( LDual ` W )
lkr0f2.o 
|- .0. = ( 0g ` D )
lkr0f2.w 
|- ( ph -> W e. LMod )
lkr0f2.g 
|- ( ph -> G e. F )
Assertion lkr0f2 
|- ( ph -> ( ( K ` G ) = V <-> G = .0. ) )

Proof

Step Hyp Ref Expression
1 lkr0f2.v 
 |-  V = ( Base ` W )
2 lkr0f2.f 
 |-  F = ( LFnl ` W )
3 lkr0f2.k 
 |-  K = ( LKer ` W )
4 lkr0f2.d 
 |-  D = ( LDual ` W )
5 lkr0f2.o 
 |-  .0. = ( 0g ` D )
6 lkr0f2.w 
 |-  ( ph -> W e. LMod )
7 lkr0f2.g 
 |-  ( ph -> G e. F )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
10 8 9 1 2 3 lkr0f 
 |-  ( ( W e. LMod /\ G e. F ) -> ( ( K ` G ) = V <-> G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
11 6 7 10 syl2anc 
 |-  ( ph -> ( ( K ` G ) = V <-> G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
12 1 8 9 4 5 6 ldual0v 
 |-  ( ph -> .0. = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) )
13 12 eqeq2d 
 |-  ( ph -> ( G = .0. <-> G = ( V X. { ( 0g ` ( Scalar ` W ) ) } ) ) )
14 11 13 bitr4d 
 |-  ( ph -> ( ( K ` G ) = V <-> G = .0. ) )