Definition df-0o 8404

Description: Define the zero operator between two normed complex vector spaces.

Assertion

Ref	Expression
df-0o	|- 0op = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = ((Base` u) X. {(0v` w)}))}

Distinct variable group:   u,o,w

Detailed syntax breakdown of Definition df-0o

Step	Hyp	Ref	Expression
1		c0o 8400	. 2 class 0op
2		vu	. . . . . . 7 set u
3	2	cv 957	. . . . . 6 class u
4		cnv 8199	. . . . . 6 class NrmCVec
5	3, 4	wcel 960	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 957	. . . . . 6 class w
8	7, 4	wcel 960	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 223	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vo	. . . . . 6 set o
11	10	cv 957	. . . . 5 class o
12		cba 8201	. . . . . . 7 class Base
13	3, 12	cfv 3188	. . . . . 6 class (Base` u)
14		cn0v 8203	. . . . . . . 8 class 0v
15	7, 14	cfv 3188	. . . . . . 7 class (0v` w)
16	15	csn 2413	. . . . . 6 class {(0v` w)}
17	13, 16	cxp 3174	. . . . 5 class ((Base` u) X. {(0v` w)})
18	11, 17	wceq 958	. . . 4 wff o = ((Base` u) X. {(0v` w)})
19	9, 18	wa 223	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ o = ((Base` u) X. {(0v` w)}))
20	19, 2, 6, 10	copab2 3970	. 2 class {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = ((Base` u) X. {(0v` w)}))}
21	1, 20	wceq 958	1 wff 0op = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = ((Base` u) X. {(0v` w)}))}

This definition is referenced by:  0ofval 8443

Copyright terms: Public domain