Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lkrscss Structured version   Unicode version

Theorem lkrscss 29823
 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.)
Hypotheses
Ref Expression
lkrsc.v
lkrsc.d Scalar
lkrsc.k
lkrsc.t
lkrsc.f LFnl
lkrsc.l LKer
lkrsc.w
lkrsc.g
lkrsc.r
Assertion
Ref Expression
lkrscss

Proof of Theorem lkrscss
StepHypRef Expression
1 lkrsc.v . . . . . 6
2 lkrsc.f . . . . . 6 LFnl
3 lkrsc.l . . . . . 6 LKer
4 lkrsc.w . . . . . . 7
5 lveclmod 16170 . . . . . . 7
64, 5syl 16 . . . . . 6
7 lkrsc.g . . . . . 6
81, 2, 3, 6, 7lkrssv 29821 . . . . 5
9 lkrsc.d . . . . . . . 8 Scalar
10 lkrsc.k . . . . . . . 8
11 lkrsc.t . . . . . . . 8
12 eqid 2435 . . . . . . . 8
131, 9, 2, 10, 11, 12, 6, 7lfl0sc 29807 . . . . . . 7
1413fveq2d 5724 . . . . . 6
15 eqid 2435 . . . . . . 7
169, 12, 1, 2lfl0f 29794 . . . . . . . . 9
176, 16syl 16 . . . . . . . 8
189, 12, 1, 2, 3lkr0f 29819 . . . . . . . 8
196, 17, 18syl2anc 643 . . . . . . 7
2015, 19mpbiri 225 . . . . . 6
2114, 20eqtr2d 2468 . . . . 5
228, 21sseqtrd 3376 . . . 4
24 sneq 3817 . . . . . . 7
2524xpeq2d 4894 . . . . . 6
2625oveq2d 6089 . . . . 5
2726fveq2d 5724 . . . 4