Theorem hh0oi

Description: The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnmo.1	|- U = <. <. +h , .h >. , normh >.
	hh0o.2	|- Z = ( U 0op U )
Assertion	hh0oi	|- 0hop = Z

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	|- U = <. <. +h , .h >. , normh >.
2		hh0o.2	|- Z = ( U 0op U )
3	1	hhba	|- ~H = ( BaseSet ` U )
4		df-ch0	|- 0H = { 0h }
5	1	hh0v	|- 0h = ( 0vec ` U )
6	5	sneqi	|- { 0h } = { ( 0vec ` U ) }
7	4 6	eqtri	|- 0H = { ( 0vec ` U ) }
8	3 7	xpeq12i	|- ( ~H X. 0H ) = ( ( BaseSet ` U ) X. { ( 0vec ` U ) } )
9		df0op2	|- 0hop = ( ~H X. 0H )
10	1	hhnv	|- U e. NrmCVec
11		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
12		eqid	|- ( 0vec ` U ) = ( 0vec ` U )
13	11 12 2	0ofval	|- ( ( U e. NrmCVec /\ U e. NrmCVec ) -> Z = ( ( BaseSet ` U ) X. { ( 0vec ` U ) } ) )
14	10 10 13	mp2an	|- Z = ( ( BaseSet ` U ) X. { ( 0vec ` U ) } )
15	8 9 14	3eqtr4i	|- 0hop = Z