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

Metamath Proof Explorer

Definition df-hodif

Description: Define the difference of two Hilbert space operators. Definition of Beran p. 111. (Contributed by NM, 9-Nov-2000) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-hodif	$⊢ -_{op} = (f \in (ℋ^{ℋ}), g \in (ℋ^{ℋ}) ⟼ (x \in ℋ ⟼ f (x) -_{ℎ} g (x)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chod	$class -_{op}$
1		vf	$setvar f$
2		chba	$class ℋ$
3		cmap	$class ↑_{𝑚}$
4	2 2 3	co	$class (ℋ^{ℋ})$
5		vg	$setvar g$
6		vx	$setvar x$
7	1	cv	$setvar f$
8	6	cv	$setvar x$
9	8 7	cfv	$class f (x)$
10		cmv	$class -_{ℎ}$
11	5	cv	$setvar g$
12	8 11	cfv	$class g (x)$
13	9 12 10	co	$class (f (x) -_{ℎ} g (x))$
14	6 2 13	cmpt	$class (x \in ℋ ⟼ f (x) -_{ℎ} g (x))$
15	1 5 4 4 14	cmpo	$class (f \in (ℋ^{ℋ}), g \in (ℋ^{ℋ}) ⟼ (x \in ℋ ⟼ f (x) -_{ℎ} g (x)))$
16	0 15	wceq	$wff -_{op} = (f \in (ℋ^{ℋ}), g \in (ℋ^{ℋ}) ⟼ (x \in ℋ ⟼ f (x) -_{ℎ} g (x)))$