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

Metamath Proof Explorer

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 : ℋ ⟶ ℋ$
		hoeq.2	$⊢ T : ℋ ⟶ ℋ$
	Assertion	hosubcli	$⊢ (S -_{op} T) : ℋ ⟶ ℋ$

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	$⊢ S : ℋ ⟶ ℋ$
2		hoeq.2	$⊢ T : ℋ ⟶ ℋ$
3		hodmval	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S -_{op} T = (x \in ℋ ⟼ S (x) -_{ℎ} T (x))$
4	1 2 3	mp2an	$⊢ S -_{op} T = (x \in ℋ ⟼ S (x) -_{ℎ} T (x))$
5	1	ffvelcdmi	$⊢ x \in ℋ \to S (x) \in ℋ$
6	2	ffvelcdmi	$⊢ x \in ℋ \to T (x) \in ℋ$
7		hvsubcl	$⊢ (S (x) \in ℋ \land T (x) \in ℋ) \to S (x) -_{ℎ} T (x) \in ℋ$
8	5 6 7	syl2anc	$⊢ x \in ℋ \to S (x) -_{ℎ} T (x) \in ℋ$
9	4 8	fmpti	$⊢ (S -_{op} T) : ℋ ⟶ ℋ$