bdophdi

Description: The difference between two bounded linear operators is bounded. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		nmoptri.1	$⊢ S \in BndLinOp$
2		nmoptri.2	$⊢ T \in BndLinOp$
3		bdopf	$⊢ S \in BndLinOp \to S : ℋ ⟶ ℋ$
4	1 3	ax-mp	$⊢ S : ℋ ⟶ ℋ$
5		bdopf	$⊢ T \in BndLinOp \to T : ℋ ⟶ ℋ$
6	2 5	ax-mp	$⊢ T : ℋ ⟶ ℋ$
7	4 6	honegsubi	$⊢ S +_{op} (-1 \cdot_{op} T) = S -_{op} T$
8		neg1cn	$⊢ - 1 \in ℂ$
9	2	bdophmi	$⊢ - 1 \in ℂ \to -1 \cdot_{op} T \in BndLinOp$
10	8 9	ax-mp	$⊢ -1 \cdot_{op} T \in BndLinOp$
11	1 10	bdophsi	$⊢ S +_{op} (-1 \cdot_{op} T) \in BndLinOp$
12	7 11	eqeltrri	$⊢ S -_{op} T \in BndLinOp$

Metamath Proof Explorer