Theorem lkrss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015)

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

Proof

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