Description: The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007) (Revised by Mario Carneiro, 18-Nov-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lno0.1 | |
|
lno0.2 | |
||
lno0.5 | |
||
lno0.z | |
||
lno0.7 | |
||
Assertion | lno0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lno0.1 | |
|
2 | lno0.2 | |
|
3 | lno0.5 | |
|
4 | lno0.z | |
|
5 | lno0.7 | |
|
6 | neg1cn | |
|
7 | 6 | a1i | |
8 | 1 3 | nvzcl | |
9 | 8 | 3ad2ant1 | |
10 | 7 9 9 | 3jca | |
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | 1 2 11 12 13 14 5 | lnolin | |
16 | 10 15 | mpdan | |
17 | 1 11 13 3 | nvlinv | |
18 | 8 17 | mpdan | |
19 | 18 | fveq2d | |
20 | 19 | 3ad2ant1 | |
21 | simp2 | |
|
22 | 1 2 5 | lnof | |
23 | 22 9 | ffvelcdmd | |
24 | 2 12 14 4 | nvlinv | |
25 | 21 23 24 | syl2anc | |
26 | 16 20 25 | 3eqtr3d | |