# Metamath Proof Explorer

Description: Associative-type law for addition and subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoaddsubass ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}={S}{+}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$

### Proof

Step Hyp Ref Expression
1 ho0f ${⊢}{0}_{\mathrm{hop}}:ℋ⟶ℋ$
2 hosubcl ${⊢}\left({0}_{\mathrm{hop}}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
3 1 2 mpan ${⊢}{U}:ℋ⟶ℋ\to \left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
4 hoaddass ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge \left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)={S}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)\right)$
5 3 4 syl3an3 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)={S}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)\right)$
6 hoaddcl ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
7 ho0sub ${⊢}\left(\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}=\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
8 6 7 stoic3 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}=\left({S}{+}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
9 ho0sub ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}{U}={T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
10 9 3adant1 ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{-}_{\mathrm{op}}{U}={T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)$
11 10 oveq2d ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {S}{+}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)={S}{+}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left({0}_{\mathrm{hop}}{-}_{\mathrm{op}}{U}\right)\right)$
12 5 8 11 3eqtr4d ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}{U}={S}{+}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$