Definition 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	|- 0op = ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0o	|- 0op
1		vu	|- u
2		cnv	|- NrmCVec
3		vw	|- w
4		cba	|- BaseSet
5	1	cv	|- u
6	5 4	cfv	|- ( BaseSet ` u )
7		cn0v	|- 0vec
8	3	cv	|- w
9	8 7	cfv	|- ( 0vec ` w )
10	9	csn	|- { ( 0vec ` w ) }
11	6 10	cxp	|- ( ( BaseSet ` u ) X. { ( 0vec ` w ) } )
12	1 3 2 2 11	cmpo	|- ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )
13	0 12	wceq	|- 0op = ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )