# Metamath Proof Explorer

## Theorem hosd1i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
Assertion hosd1i ${⊢}{T}{+}_{\mathrm{op}}{U}={T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$

### Proof

Step Hyp Ref Expression
1 hosd1.2 ${⊢}{T}:ℋ⟶ℋ$
2 hosd1.3 ${⊢}{U}:ℋ⟶ℋ$
3 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
4 3 2 hosubcli ${⊢}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
5 1 2 hoaddcli ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
6 4 5 hoaddcomi ${⊢}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)=\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
7 5 3 2 hoaddsubassi ${⊢}\left(\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{U}=\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
8 6 7 eqtr4i ${⊢}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)=\left(\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{U}$
9 5 hoaddid1i ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}={T}{+}_{\mathrm{op}}{U}$
10 9 oveq1i ${⊢}\left(\left({T}{+}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{0}_{\mathrm{hop}}\right){-}_{\mathrm{op}}{U}=\left({T}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}$
11 1 2 2 hoaddsubi ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}=\left({T}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{U}$
12 1 2 hosubcli ${⊢}\left({T}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
13 12 2 hoaddcomi ${⊢}\left({T}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}{U}={U}{+}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
14 2 1 hodseqi ${⊢}{U}{+}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)={T}$
15 11 13 14 3eqtri ${⊢}\left({T}{+}_{\mathrm{op}}{U}\right){-}_{\mathrm{op}}{U}={T}$
16 8 10 15 3eqtri ${⊢}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)={T}$
17 1 4 5 hodsi ${⊢}{T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}↔\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right){+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)={T}$
18 16 17 mpbir ${⊢}{T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)={T}{+}_{\mathrm{op}}{U}$
19 18 eqcomi ${⊢}{T}{+}_{\mathrm{op}}{U}={T}{-}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$