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

Proof

Step	Hyp	Ref	Expression
1		ldualkrsc.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldualkrsc.k	$$⊢K={\mathrm{Base}}_R$$
3		ldualkrsc.o	$$⊢\underset{\dot{}}{0}=0_R$$
4		ldualkrsc.f	$$⊢F=\mathrm{LFnl}\left(W\right)$$
5		ldualkrsc.l	$$⊢L=\mathrm{LKer}\left(W\right)$$
6		ldualkrsc.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
7		ldualkrsc.s	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
8		ldualkrsc.w	$$⊢\phi \to W\in \mathrm{LVec}$$
9		ldualkrsc.g	$$⊢\phi \to G\in F$$
10		ldualkrsc.x	$$⊢\phi \to X\in K$$
11		ldualkrsc.e	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
12		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
13		eqid	$$⊢{\cdot }_R={\cdot }_R$$
14	4 12 1 2 13 6 7 8 10 9	ldualvs	$$⊢\phi \to X\underset{\dot{}}{·}G=G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)$$
15	14	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)$$
16	12 1 2 13 4 5 8 9 10 3 11	lkrsc	$$⊢\phi \to L\left(G{{\cdot }_R}_f\left({\mathrm{Base}}_W\times \left\{X\right\}\right)\right)=L\left(G\right)$$
17	15 16	eqtrd	$$⊢\phi \to L\left(X\underset{\dot{}}{·}G\right)=L\left(G\right)$$