Metamath Proof Explorer


Theorem hoaddridi

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 T:
Assertion hoaddridi T+op0hop=T

Proof

Step Hyp Ref Expression
1 hoaddrid.1 T:
2 ho0f 0hop:
3 hosval T:0hop:xT+op0hopx=Tx+0hopx
4 1 2 3 mp3an12 xT+op0hopx=Tx+0hopx
5 ho0val x0hopx=0
6 5 oveq2d xTx+0hopx=Tx+0
7 1 ffvelcdmi xTx
8 ax-hvaddid TxTx+0=Tx
9 7 8 syl xTx+0=Tx
10 4 6 9 3eqtrd xT+op0hopx=Tx
11 10 rgen xT+op0hopx=Tx
12 1 2 hoaddcli T+op0hop:
13 12 1 hoeqi xT+op0hopx=TxT+op0hop=T
14 11 13 mpbi T+op0hop=T