Metamath Proof Explorer

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 ${⊢}{0}_{\mathrm{op}}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0o ${class}{0}_{\mathrm{op}}$
1 vu ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 vw ${setvar}{w}$
4 cba ${class}\mathrm{BaseSet}$
5 1 cv ${setvar}{u}$
6 5 4 cfv ${class}\mathrm{BaseSet}\left({u}\right)$
7 cn0v ${class}{0}_{\mathrm{vec}}$
8 3 cv ${setvar}{w}$
9 8 7 cfv ${class}{0}_{\mathrm{vec}}\left({w}\right)$
10 9 csn ${class}\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}$
11 6 10 cxp ${class}\left(\mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}\right)$
12 1 3 2 2 11 cmpo ${class}\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}\right)$
13 0 12 wceq ${wff}{0}_{\mathrm{op}}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\mathrm{BaseSet}\left({u}\right)×\left\{{0}_{\mathrm{vec}}\left({w}\right)\right\}\right)$