Theorem hodcli

Description: Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoeq.1	|- S : ~H --> ~H
	hoeq.2	|- T : ~H --> ~H
Assertion	hodcli	|- ( A e. ~H -> ( ( S -op T ) ` A ) e. ~H )

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	|- S : ~H --> ~H
2		hoeq.2	|- T : ~H --> ~H
3		hodcl	|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ A e. ~H ) -> ( ( S -op T ) ` A ) e. ~H )
4	1 2 3	mpanl12	|- ( A e. ~H -> ( ( S -op T ) ` A ) e. ~H )