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. ) )