Definition df-0o 26986

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 26982	. 2 class 0op
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 26823	. . 3 class NrmCVec
5	2	cv 1474	. . . . 5 class 𝑢
6		cba 26825	. . . . 5 class BaseSet
7	5, 6	cfv 5804	. . . 4 class (BaseSet‘𝑢)
8	3	cv 1474	. . . . . 6 class 𝑤
9		cn0v 26827	. . . . . 6 class 0vec
10	8, 9	cfv 5804	. . . . 5 class (0vec‘𝑤)
11	10	csn 4125	. . . 4 class {(0vec‘𝑤)}
12	7, 11	cxp 5036	. . 3 class ((BaseSet‘𝑢) × {(0vec‘𝑤)})
13	2, 3, 4, 4, 12	cmpt2 6551	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)}))
14	1, 13	wceq 1475	1 wff 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)}))

This definition is referenced by:  0ofval  27026