This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℋ → R ∘ S ∘ T ⁡ A = R ⁡ S ⁡ T ⁡ A

Proof

Step Hyp Ref Expression
1 hods.1 ⊢ R : ℋ ⟶ ℋ
2 hods.2 ⊢ S : ℋ ⟶ ℋ
3 hods.3 ⊢ T : ℋ ⟶ ℋ
4 1 2 hocofi ⊢ R ∘ S : ℋ ⟶ ℋ
5 4 3 hocoi ⊢ A ∈ ℋ → R ∘ S ∘ T ⁡ A = R ∘ S ⁡ T ⁡ A
6 3 ffvelcdmi ⊢ A ∈ ℋ → T ⁡ A ∈ ℋ
7 1 2 hocoi ⊢ T ⁡ A ∈ ℋ → R ∘ S ⁡ T ⁡ A = R ⁡ S ⁡ T ⁡ A
8 6 7 syl ⊢ A ∈ ℋ → R ∘ S ⁡ T ⁡ A = R ⁡ S ⁡ T ⁡ A
9 5 8 eqtrd ⊢ A ∈ ℋ → R ∘ S ∘ T ⁡ A = R ⁡ S ⁡ T ⁡ A