Theorem ldualkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014)

	Ref	Expression
Hypotheses	ldualkrsc.r	|- R = ( Scalar ` W )
	ldualkrsc.k	|- K = ( Base ` R )
	ldualkrsc.o	|- .0. = ( 0g ` R )
	ldualkrsc.f	|- F = ( LFnl ` W )
	ldualkrsc.l	|- L = ( LKer ` W )
	ldualkrsc.d	|- D = ( LDual ` W )
	ldualkrsc.s	|- .x. = ( .s ` D )
	ldualkrsc.w	|- ( ph -> W e. LVec )
	ldualkrsc.g	|- ( ph -> G e. F )
	ldualkrsc.x	|- ( ph -> X e. K )
	ldualkrsc.e	|- ( ph -> X =/= .0. )
Assertion	ldualkrsc	|- ( ph -> ( L ` ( X .x. G ) ) = ( L ` G ) )

Proof

Step	Hyp	Ref	Expression
1		ldualkrsc.r	|- R = ( Scalar ` W )
2		ldualkrsc.k	|- K = ( Base ` R )
3		ldualkrsc.o	|- .0. = ( 0g ` R )
4		ldualkrsc.f	|- F = ( LFnl ` W )
5		ldualkrsc.l	|- L = ( LKer ` W )
6		ldualkrsc.d	|- D = ( LDual ` W )
7		ldualkrsc.s	|- .x. = ( .s ` D )
8		ldualkrsc.w	|- ( ph -> W e. LVec )
9		ldualkrsc.g	|- ( ph -> G e. F )
10		ldualkrsc.x	|- ( ph -> X e. K )
11		ldualkrsc.e	|- ( ph -> X =/= .0. )
12		eqid	|- ( Base ` W ) = ( Base ` W )
13		eqid	|- ( .r ` R ) = ( .r ` R )
14	4 12 1 2 13 6 7 8 10 9	ldualvs	|- ( ph -> ( X .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
15	14	fveq2d	|- ( ph -> ( L ` ( X .x. G ) ) = ( L ` ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) )
16	12 1 2 13 4 5 8 9 10 3 11	lkrsc	|- ( ph -> ( L ` ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) ) = ( L ` G ) )
17	15 16	eqtrd	|- ( ph -> ( L ` ( X .x. G ) ) = ( L ` G ) )