# Metamath Proof Explorer

Description: Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hods.1 ${⊢}{R}:ℋ⟶ℋ$
hods.2 ${⊢}{S}:ℋ⟶ℋ$
hods.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion hoaddassi ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$

### Proof

Step Hyp Ref Expression
1 hods.1 ${⊢}{R}:ℋ⟶ℋ$
2 hods.2 ${⊢}{S}:ℋ⟶ℋ$
3 hods.3 ${⊢}{T}:ℋ⟶ℋ$
4 hosval ${⊢}\left({R}:ℋ⟶ℋ\wedge {S}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({R}{+}_{\mathrm{op}}{S}\right)\left({x}\right)={R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)$
5 1 2 4 mp3an12 ${⊢}{x}\in ℋ\to \left({R}{+}_{\mathrm{op}}{S}\right)\left({x}\right)={R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)$
6 5 oveq1d ${⊢}{x}\in ℋ\to \left({R}{+}_{\mathrm{op}}{S}\right)\left({x}\right){+}_{ℎ}{T}\left({x}\right)=\left({R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)\right){+}_{ℎ}{T}\left({x}\right)$
7 1 2 hoaddcli ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
8 hosval ${⊢}\left(\left({R}{+}_{\mathrm{op}}{S}\right):ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right)\left({x}\right)=\left({R}{+}_{\mathrm{op}}{S}\right)\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
9 7 3 8 mp3an12 ${⊢}{x}\in ℋ\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right)\left({x}\right)=\left({R}{+}_{\mathrm{op}}{S}\right)\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
10 hosval ${⊢}\left({S}:ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
11 2 3 10 mp3an12 ${⊢}{x}\in ℋ\to \left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)$
12 11 oveq2d ${⊢}{x}\in ℋ\to {R}\left({x}\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)={R}\left({x}\right){+}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
13 2 3 hoaddcli ${⊢}\left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
14 hosval ${⊢}\left({R}:ℋ⟶ℋ\wedge \left({S}{+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)={R}\left({x}\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)$
15 1 13 14 mp3an12 ${⊢}{x}\in ℋ\to \left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)={R}\left({x}\right){+}_{ℎ}\left({S}{+}_{\mathrm{op}}{T}\right)\left({x}\right)$
16 1 ffvelrni ${⊢}{x}\in ℋ\to {R}\left({x}\right)\in ℋ$
17 2 ffvelrni ${⊢}{x}\in ℋ\to {S}\left({x}\right)\in ℋ$
18 3 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
19 ax-hvass ${⊢}\left({R}\left({x}\right)\in ℋ\wedge {S}\left({x}\right)\in ℋ\wedge {T}\left({x}\right)\in ℋ\right)\to \left({R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)\right){+}_{ℎ}{T}\left({x}\right)={R}\left({x}\right){+}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
20 16 17 18 19 syl3anc ${⊢}{x}\in ℋ\to \left({R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)\right){+}_{ℎ}{T}\left({x}\right)={R}\left({x}\right){+}_{ℎ}\left({S}\left({x}\right){+}_{ℎ}{T}\left({x}\right)\right)$
21 12 15 20 3eqtr4d ${⊢}{x}\in ℋ\to \left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)=\left({R}\left({x}\right){+}_{ℎ}{S}\left({x}\right)\right){+}_{ℎ}{T}\left({x}\right)$
22 6 9 21 3eqtr4d ${⊢}{x}\in ℋ\to \left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right)\left({x}\right)=\left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)$
23 22 rgen ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right)\left({x}\right)=\left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)$
24 7 3 hoaddcli ${⊢}\left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
25 1 13 hoaddcli ${⊢}\left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right):ℋ⟶ℋ$
26 24 25 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}\right)\left({x}\right)=\left({R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)\right)\left({x}\right)↔\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$
27 23 26 mpbi ${⊢}\left({R}{+}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{T}={R}{+}_{\mathrm{op}}\left({S}{+}_{\mathrm{op}}{T}\right)$