Metamath Proof Explorer


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=ScalarW
ldualkrsc.k K=BaseR
ldualkrsc.o 0˙=0R
ldualkrsc.f F=LFnlW
ldualkrsc.l L=LKerW
ldualkrsc.d D=LDualW
ldualkrsc.s ·˙=D
ldualkrsc.w φWLVec
ldualkrsc.g φGF
ldualkrsc.x φXK
ldualkrsc.e φX0˙
Assertion ldualkrsc φLX·˙G=LG

Proof

Step Hyp Ref Expression
1 ldualkrsc.r R=ScalarW
2 ldualkrsc.k K=BaseR
3 ldualkrsc.o 0˙=0R
4 ldualkrsc.f F=LFnlW
5 ldualkrsc.l L=LKerW
6 ldualkrsc.d D=LDualW
7 ldualkrsc.s ·˙=D
8 ldualkrsc.w φWLVec
9 ldualkrsc.g φGF
10 ldualkrsc.x φXK
11 ldualkrsc.e φX0˙
12 eqid BaseW=BaseW
13 eqid R=R
14 4 12 1 2 13 6 7 8 10 9 ldualvs φX·˙G=GRfBaseW×X
15 14 fveq2d φLX·˙G=LGRfBaseW×X
16 12 1 2 13 4 5 8 9 10 3 11 lkrsc φLGRfBaseW×X=LG
17 15 16 eqtrd φLX·˙G=LG