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

Metamath Proof Explorer

Theorem hoaddfni

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

Ref Expression
Hypotheses hoeq.1 ⊢ 𝑆 : ℋ ⟶ ℋ
hoeq.2 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hoaddfni ( 𝑆 +op 𝑇 ) Fn ℋ

Proof

Step Hyp Ref Expression
1 hoeq.1 ⊢ 𝑆 : ℋ ⟶ ℋ
2 hoeq.2 ⊢ 𝑇 : ℋ ⟶ ℋ
3 1 2 hoaddcli ⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
4 ffn ⊢ ( ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ → ( 𝑆 +op 𝑇 ) Fn ℋ )
5 3 4 ax-mp ⊢ ( 𝑆 +op 𝑇 ) Fn ℋ