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

Metamath Proof Explorer

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 : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} T) : ℋ ⟶ ℋ$

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	$⊢ (S : ℋ ⟶ ℋ \land x \in ℋ) \to S (x) \in ℋ$
2	1	adantlr	$⊢ ((S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to S (x) \in ℋ$
3		ffvelcdm	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to T (x) \in ℋ$
4	3	adantll	$⊢ ((S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to T (x) \in ℋ$
5		hvaddcl	$⊢ (S (x) \in ℋ \land T (x) \in ℋ) \to S (x) +_{ℎ} T (x) \in ℋ$
6	2 4 5	syl2anc	$⊢ ((S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to S (x) +_{ℎ} T (x) \in ℋ$
7	6	fmpttd	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (x \in ℋ ⟼ S (x) +_{ℎ} T (x)) : ℋ ⟶ ℋ$
8		hosmval	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S +_{op} T = (x \in ℋ ⟼ S (x) +_{ℎ} T (x))$
9	8	feq1d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to ((S +_{op} T) : ℋ ⟶ ℋ \leftrightarrow (x \in ℋ ⟼ S (x) +_{ℎ} T (x)) : ℋ ⟶ ℋ)$
10	7 9	mpbird	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} T) : ℋ ⟶ ℋ$