Definition df-0o 28518

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

Distinct variable group:   𝑤,𝑢

Detailed syntax breakdown of Definition df-0o

Step	Hyp	Ref	Expression
1		c0o 28514	. 2 class 0op
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 28355	. . 3 class NrmCVec
5	2	cv 1532	. . . . 5 class 𝑢
6		cba 28357	. . . . 5 class BaseSet
7	5, 6	cfv 6350	. . . 4 class (BaseSet‘𝑢)
8	3	cv 1532	. . . . . 6 class 𝑤
9		cn0v 28359	. . . . . 6 class 0vec
10	8, 9	cfv 6350	. . . . 5 class (0vec‘𝑤)
11	10	csn 4561	. . . 4 class {(0vec‘𝑤)}
12	7, 11	cxp 5548	. . 3 class ((BaseSet‘𝑢) × {(0vec‘𝑤)})
13	2, 3, 4, 4, 12	cmpo 7152	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)}))
14	1, 13	wceq 1533	1 wff 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)}))

This definition is referenced by:  0ofval  28558