Theorem hoaddcl

Description: The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hoaddcl	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) : ~H --> ~H )

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	|- ( ( S : ~H --> ~H /\ x e. ~H ) -> ( S ` x ) e. ~H )
2	1	adantlr	|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( S ` x ) e. ~H )
3		ffvelrn	|- ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
4	3	adantll	|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( T ` x ) e. ~H )
5		hvaddcl	|- ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( S ` x ) +h ( T ` x ) ) e. ~H )
6	2 4 5	syl2anc	|- ( ( ( S : ~H --> ~H /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( S ` x ) +h ( T ` x ) ) e. ~H )
7	6	fmpttd	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( x e. ~H |-> ( ( S ` x ) +h ( T ` x ) ) ) : ~H --> ~H )
8		hosmval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( x e. ~H |-> ( ( S ` x ) +h ( T ` x ) ) ) )
9	8	feq1d	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S +op T ) : ~H --> ~H <-> ( x e. ~H |-> ( ( S ` x ) +h ( T ` x ) ) ) : ~H --> ~H ) )
10	7 9	mpbird	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) : ~H --> ~H )