# Metamath Proof Explorer

## Theorem hosubdi

Description: Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hosubdi ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({A}{·}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$

### Proof

Step Hyp Ref Expression
1 neg1cn ${⊢}-1\in ℂ$
2 homulcl ${⊢}\left(-1\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
3 1 2 mpan ${⊢}{U}:ℋ⟶ℋ\to \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
4 hoadddi ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge \left(-1{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)$
5 3 4 syl3an3 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)$
6 homul12 ${⊢}\left({A}\in ℂ\wedge -1\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)=-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
7 1 6 mp3an2 ${⊢}\left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)=-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
8 7 3adant2 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)=-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
9 8 oveq2d ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)$
10 5 9 eqtrd ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)$
11 honegsub ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)={T}{-}_{\mathrm{op}}{U}$
12 11 oveq2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={A}{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
13 12 3adant1 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}{U}\right)\right)={A}{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)$
14 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
15 homulcl ${⊢}\left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
16 honegsub ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
17 14 15 16 syl2an ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
18 17 3impdi ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left(-1{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)=\left({A}{·}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$
19 10 13 18 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({T}{-}_{\mathrm{op}}{U}\right)=\left({A}{·}_{\mathrm{op}}{T}\right){-}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)$