Theorem hosubcli

Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoeq.1	|- S : ~H --> ~H
	hoeq.2	|- T : ~H --> ~H
Assertion	hosubcli	|- ( S -op T ) : ~H --> ~H

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	|- S : ~H --> ~H
2		hoeq.2	|- T : ~H --> ~H
3		hodmval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) ) )
4	1 2 3	mp2an	|- ( S -op T ) = ( x e. ~H |-> ( ( S ` x ) -h ( T ` x ) ) )
5	1	ffvelcdmi	|- ( x e. ~H -> ( S ` x ) e. ~H )
6	2	ffvelcdmi	|- ( x e. ~H -> ( T ` x ) e. ~H )
7		hvsubcl	|- ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( S ` x ) -h ( T ` x ) ) e. ~H )
8	5 6 7	syl2anc	|- ( x e. ~H -> ( ( S ` x ) -h ( T ` x ) ) e. ~H )
9	4 8	fmpti	|- ( S -op T ) : ~H --> ~H