Metamath Proof Explorer


Theorem lkrscss

Description: The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014)

Ref Expression
Hypotheses lkrsc.v V=BaseW
lkrsc.d D=ScalarW
lkrsc.k K=BaseD
lkrsc.t ·˙=D
lkrsc.f F=LFnlW
lkrsc.l L=LKerW
lkrsc.w φWLVec
lkrsc.g φGF
lkrsc.r φRK
Assertion lkrscss φLGLG·˙fV×R

Proof

Step Hyp Ref Expression
1 lkrsc.v V=BaseW
2 lkrsc.d D=ScalarW
3 lkrsc.k K=BaseD
4 lkrsc.t ·˙=D
5 lkrsc.f F=LFnlW
6 lkrsc.l L=LKerW
7 lkrsc.w φWLVec
8 lkrsc.g φGF
9 lkrsc.r φRK
10 lveclmod WLVecWLMod
11 7 10 syl φWLMod
12 1 5 6 11 8 lkrssv φLGV
13 eqid 0D=0D
14 1 2 5 3 4 13 11 8 lfl0sc φG·˙fV×0D=V×0D
15 14 fveq2d φLG·˙fV×0D=LV×0D
16 eqid V×0D=V×0D
17 2 13 1 5 lfl0f WLModV×0DF
18 2 13 1 5 6 lkr0f WLModV×0DFLV×0D=VV×0D=V×0D
19 11 17 18 syl2anc2 φLV×0D=VV×0D=V×0D
20 16 19 mpbiri φLV×0D=V
21 15 20 eqtr2d φV=LG·˙fV×0D
22 12 21 sseqtrd φLGLG·˙fV×0D
23 22 adantr φR=0DLGLG·˙fV×0D
24 sneq R=0DR=0D
25 24 xpeq2d R=0DV×R=V×0D
26 25 oveq2d R=0DG·˙fV×R=G·˙fV×0D
27 26 fveq2d R=0DLG·˙fV×R=LG·˙fV×0D
28 27 adantl φR=0DLG·˙fV×R=LG·˙fV×0D
29 23 28 sseqtrrd φR=0DLGLG·˙fV×R
30 7 adantr φR0DWLVec
31 8 adantr φR0DGF
32 9 adantr φR0DRK
33 simpr φR0DR0D
34 1 2 3 4 5 6 30 31 32 13 33 lkrsc φR0DLG·˙fV×R=LG
35 eqimss2 LG·˙fV×R=LGLGLG·˙fV×R
36 34 35 syl φR0DLGLG·˙fV×R
37 29 36 pm2.61dane φLGLG·˙fV×R