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=\mathrm{Scalar}\left(W\right)$$
	lkrss.k	$$⊢K={\mathrm{Base}}_R$$
	lkrss.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
	lkrss.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
	lkrss.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	lkrss.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lkrss.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lkrss.g	$$⊢\phi \to G\in F$$
	lkrss.x	$$⊢\phi \to X\in K$$
Assertion	lkrss	$$⊢\phi \to L\left(G\right)\subseteq L\left(X\underset{\dot{}}{·}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lkrss.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		lkrss.k	$$⊢K={\mathrm{Base}}_R$$
3		lkrss.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
4		lkrss.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
5		lkrss.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
6		lkrss.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
7		lkrss.w	$$⊢\phi \to W\in \mathrm{LVec}$$
8		lkrss.g	$$⊢\phi \to G\in F$$
9		lkrss.x	$$⊢\phi \to X\in K$$
10		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12	10 1 2 11 3 4 7 8 9	lkrscss	$$⊢\phi \to L\left(G\right)\subseteq L\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right)$$
13	3 10 1 2 11 5 6 7 9 8	ldualvs	$$⊢\phi \to X\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)$$
14	13	fveq2d	$$⊢\phi \to L\left(X\underset{\dot{}}{·}G\right)=L\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right)$$
15	12 14	sseqtrrd	$$⊢\phi \to L\left(G\right)\subseteq L\left(X\underset{\dot{}}{·}G\right)$$