# Metamath Proof Explorer

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

Ref Expression
Assertion hoadddi ${⊢}\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 simpl1 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}\in ℂ$
2 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
3 2 3ad2antl2 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
4 ffvelrn ${⊢}\left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {U}\left({x}\right)\in ℋ$
5 4 3ad2antl3 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {U}\left({x}\right)\in ℋ$
6 ax-hvdistr1 ${⊢}\left({A}\in ℂ\wedge {T}\left({x}\right)\in ℋ\wedge {U}\left({x}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right)=\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{U}\left({x}\right)\right)$
7 1 3 5 6 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right)=\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{U}\left({x}\right)\right)$
8 hosval ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)={T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)$
9 8 oveq2d ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right)$
10 9 3expa ${⊢}\left(\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right)$
11 10 3adantl1 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\left({x}\right){+}_{ℎ}{U}\left({x}\right)\right)$
12 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
13 12 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
14 13 3adantl3 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
15 homval ${⊢}\left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}{U}\left({x}\right)$
16 15 3expa ${⊢}\left(\left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}{U}\left({x}\right)$
17 16 3adantl2 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)={A}{\cdot }_{ℎ}{U}\left({x}\right)$
18 14 17 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)=\left({A}{\cdot }_{ℎ}{T}\left({x}\right)\right){+}_{ℎ}\left({A}{\cdot }_{ℎ}{U}\left({x}\right)\right)$
19 7 11 18 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)$
20 hoaddcl ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
21 20 anim2i ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({A}\in ℂ\wedge \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)$
22 21 3impb ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}\in ℂ\wedge \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)$
23 homval ${⊢}\left({A}\in ℂ\wedge \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)$
24 23 3expa ${⊢}\left(\left({A}\in ℂ\wedge \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)$
25 22 24 sylan ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}{+}_{\mathrm{op}}{U}\right)\left({x}\right)$
26 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
27 homulcl ${⊢}\left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ$
28 26 27 anim12i ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)$
29 28 3impdi ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)$
30 hosval ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)$
31 30 3expa ${⊢}\left(\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)$
32 29 31 sylan ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({x}\right){+}_{ℎ}\left({A}{·}_{\mathrm{op}}{U}\right)\left({x}\right)$
33 19 25 32 3eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)$
34 33 ralrimiva ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)$
35 homulcl ${⊢}\left({A}\in ℂ\wedge \left({T}{+}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
36 20 35 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
37 36 3impb ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
38 hoaddcl ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}{U}\right):ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
39 26 27 38 syl2an ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({A}\in ℂ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
40 39 3impdi ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ$
41 hoeq ${⊢}\left(\left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ\wedge \left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right):ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)↔{A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)$
42 37 40 41 syl2anc ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)\right)\left({x}\right)=\left(\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)\left({x}\right)↔{A}{·}_{\mathrm{op}}\left({T}{+}_{\mathrm{op}}{U}\right)=\left({A}{·}_{\mathrm{op}}{T}\right){+}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{U}\right)\right)$
43 34 42 mpbid ${⊢}\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)$