# Metamath Proof Explorer

## Theorem ho2coi

Description: Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hods.1 ${⊢}{R}:ℋ⟶ℋ$
hods.2 ${⊢}{S}:ℋ⟶ℋ$
hods.3 ${⊢}{T}:ℋ⟶ℋ$
Assertion ho2coi ${⊢}{A}\in ℋ\to \left(\left({R}\circ {S}\right)\circ {T}\right)\left({A}\right)={R}\left({S}\left({T}\left({A}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 hods.1 ${⊢}{R}:ℋ⟶ℋ$
2 hods.2 ${⊢}{S}:ℋ⟶ℋ$
3 hods.3 ${⊢}{T}:ℋ⟶ℋ$
4 1 2 hocofi ${⊢}\left({R}\circ {S}\right):ℋ⟶ℋ$
5 4 3 hocoi ${⊢}{A}\in ℋ\to \left(\left({R}\circ {S}\right)\circ {T}\right)\left({A}\right)=\left({R}\circ {S}\right)\left({T}\left({A}\right)\right)$
6 3 ffvelrni ${⊢}{A}\in ℋ\to {T}\left({A}\right)\in ℋ$
7 1 2 hocoi ${⊢}{T}\left({A}\right)\in ℋ\to \left({R}\circ {S}\right)\left({T}\left({A}\right)\right)={R}\left({S}\left({T}\left({A}\right)\right)\right)$
8 6 7 syl ${⊢}{A}\in ℋ\to \left({R}\circ {S}\right)\left({T}\left({A}\right)\right)={R}\left({S}\left({T}\left({A}\right)\right)\right)$
9 5 8 eqtrd ${⊢}{A}\in ℋ\to \left(\left({R}\circ {S}\right)\circ {T}\right)\left({A}\right)={R}\left({S}\left({T}\left({A}\right)\right)\right)$