Definition df-h0v 10471

Description: Define the zero vector of Hilbert space. Note that 0v is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v 10668.

Assertion

Ref	Expression
df-h0v	|- 0h = (0v` <.<. +h , .h >., normh>.)

Detailed syntax breakdown of Definition df-h0v

Step	Hyp	Ref	Expression
1		c0v 10423	. 2 class 0h
2		cva 10421	. . . . 5 class +h
3		csm 10422	. . . . 5 class .h
4	2, 3	cop 3046	. . . 4 class <. +h , .h >.
5		cno 10426	. . . 4 class normh
6	4, 5	cop 3046	. . 3 class <.<. +h , .h >., normh>.
7		cn0v 9539	. . 3 class 0v
8	6, 7	cfv 3998	. 2 class (0v` <.<. +h , .h >., normh>.)
9	1, 8	wceq 1298	1 wff 0h = (0v` <.<. +h , .h >., normh>.)

This definition is referenced by:  axhv0cl 10487  axhvaddid 10488  axhvmul0 10494  axhis4 10499

Copyright terms: Public domain