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 = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0o	⊢ 0op
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vw	⊢ 𝑤
4		cba	⊢ BaseSet
5	1	cv	⊢ 𝑢
6	5 4	cfv	⊢ ( BaseSet ‘ 𝑢 )
7		cn0v	⊢ 0vec
8	3	cv	⊢ 𝑤
9	8 7	cfv	⊢ ( 0vec ‘ 𝑤 )
10	9	csn	⊢ { ( 0vec ‘ 𝑤 ) }
11	6 10	cxp	⊢ ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } )
12	1 3 2 2 11	cmpo	⊢ ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } ) )
13	0 12	wceq	⊢ 0op = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( ( BaseSet ‘ 𝑢 ) × { ( 0vec ‘ 𝑤 ) } ) )