Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | hoaddrid.1 | |
|
Assertion | hoaddridi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoaddrid.1 | |
|
2 | ho0f | |
|
3 | hosval | |
|
4 | 1 2 3 | mp3an12 | |
5 | ho0val | |
|
6 | 5 | oveq2d | |
7 | 1 | ffvelcdmi | |
8 | ax-hvaddid | |
|
9 | 7 8 | syl | |
10 | 4 6 9 | 3eqtrd | |
11 | 10 | rgen | |
12 | 1 2 | hoaddcli | |
13 | 12 1 | hoeqi | |
14 | 11 13 | mpbi | |