Definition df-0o 27602

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

Assertion

Ref	Expression
df-0o	|- 0op = ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )

Distinct variable group:   w, u

Detailed syntax breakdown of Definition df-0o

Step	Hyp	Ref	Expression
1		c0o 27598	. 2 class 0op
2		vu	. . 3 setvar u
3		vw	. . 3 setvar w
4		cnv 27439	. . 3 class NrmCVec
5	2	cv 1482	. . . . 5 class u
6		cba 27441	. . . . 5 class BaseSet
7	5, 6	cfv 5888	. . . 4 class ( BaseSet ` u )
8	3	cv 1482	. . . . . 6 class w
9		cn0v 27443	. . . . . 6 class 0vec
10	8, 9	cfv 5888	. . . . 5 class ( 0vec ` w )
11	10	csn 4177	. . . 4 class { ( 0vec ` w ) }
12	7, 11	cxp 5112	. . 3 class ( ( BaseSet ` u ) X. { ( 0vec ` w ) } )
13	2, 3, 4, 4, 12	cmpt2 6652	. 2 class ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )
14	1, 13	wceq 1483	1 wff 0op = ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )

This definition is referenced by:  0ofval  27642