df-0o

Description: Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-0o	$⊢ 0_{op} = (u \in NrmCVec, w \in NrmCVec ⟼ BaseSet (u) \times \{0_{vec} (w)\})$

Step	Hyp	Ref	Expression
0		c0o	$class 0_{op}$
1		vu	$setvar u$
2		cnv	$class NrmCVec$
3		vw	$setvar w$
4		cba	$class BaseSet$
5	1	cv	$setvar u$
6	5 4	cfv	$class BaseSet (u)$
7		cn0v	$class 0_{vec}$
8	3	cv	$setvar w$
9	8 7	cfv	$class 0_{vec} (w)$
10	9	csn	$class \{0_{vec} (w)\}$
11	6 10	cxp	$class (BaseSet (u) \times \{0_{vec} (w)\})$
12	1 3 2 2 11	cmpo	$class (u \in NrmCVec, w \in NrmCVec ⟼ BaseSet (u) \times \{0_{vec} (w)\})$
13	0 12	wceq	$wff 0_{op} = (u \in NrmCVec, w \in NrmCVec ⟼ BaseSet (u) \times \{0_{vec} (w)\})$

Metamath Proof Explorer