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 | |
|
lkrsc.d | |
||
lkrsc.k | |
||
lkrsc.t | |
||
lkrsc.f | |
||
lkrsc.l | |
||
lkrsc.w | |
||
lkrsc.g | |
||
lkrsc.r | |
||
Assertion | lkrscss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lkrsc.v | |
|
2 | lkrsc.d | |
|
3 | lkrsc.k | |
|
4 | lkrsc.t | |
|
5 | lkrsc.f | |
|
6 | lkrsc.l | |
|
7 | lkrsc.w | |
|
8 | lkrsc.g | |
|
9 | lkrsc.r | |
|
10 | lveclmod | |
|
11 | 7 10 | syl | |
12 | 1 5 6 11 8 | lkrssv | |
13 | eqid | |
|
14 | 1 2 5 3 4 13 11 8 | lfl0sc | |
15 | 14 | fveq2d | |
16 | eqid | |
|
17 | 2 13 1 5 | lfl0f | |
18 | 2 13 1 5 6 | lkr0f | |
19 | 11 17 18 | syl2anc2 | |
20 | 16 19 | mpbiri | |
21 | 15 20 | eqtr2d | |
22 | 12 21 | sseqtrd | |
23 | 22 | adantr | |
24 | sneq | |
|
25 | 24 | xpeq2d | |
26 | 25 | oveq2d | |
27 | 26 | fveq2d | |
28 | 27 | adantl | |
29 | 23 28 | sseqtrrd | |
30 | 7 | adantr | |
31 | 8 | adantr | |
32 | 9 | adantr | |
33 | simpr | |
|
34 | 1 2 3 4 5 6 30 31 32 13 33 | lkrsc | |
35 | eqimss2 | |
|
36 | 34 35 | syl | |
37 | 29 36 | pm2.61dane | |