Theorem ho2coi

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

	Ref	Expression
Hypotheses	hods.1	⊢ 𝑅 : ℋ ⟶ ℋ
	hods.2	⊢ 𝑆 : ℋ ⟶ ℋ
	hods.3	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	ho2coi	⊢ ( 𝐴 ∈ ℋ → ( ( ( 𝑅 ∘ 𝑆 ) ∘ 𝑇 ) ‘ 𝐴 ) = ( 𝑅 ‘ ( 𝑆 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hods.1	⊢ 𝑅 : ℋ ⟶ ℋ
2		hods.2	⊢ 𝑆 : ℋ ⟶ ℋ
3		hods.3	⊢ 𝑇 : ℋ ⟶ ℋ
4	1 2	hocofi	⊢ ( 𝑅 ∘ 𝑆 ) : ℋ ⟶ ℋ
5	4 3	hocoi	⊢ ( 𝐴 ∈ ℋ → ( ( ( 𝑅 ∘ 𝑆 ) ∘ 𝑇 ) ‘ 𝐴 ) = ( ( 𝑅 ∘ 𝑆 ) ‘ ( 𝑇 ‘ 𝐴 ) ) )
6	3	ffvelcdmi	⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
7	1 2	hocoi	⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( ( 𝑅 ∘ 𝑆 ) ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑅 ‘ ( 𝑆 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
8	6 7	syl	⊢ ( 𝐴 ∈ ℋ → ( ( 𝑅 ∘ 𝑆 ) ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑅 ‘ ( 𝑆 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
9	5 8	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( ( ( 𝑅 ∘ 𝑆 ) ∘ 𝑇 ) ‘ 𝐴 ) = ( 𝑅 ‘ ( 𝑆 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )