This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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