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

Metamath Proof Explorer

Theorem df0op2

Description: Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion df0op2 
|- 0hop = ( ~H X. 0H )

Proof

Step Hyp Ref Expression
1 ho0f 
 |-  0hop : ~H --> ~H
2 ffn 
 |-  ( 0hop : ~H --> ~H -> 0hop Fn ~H )
3 1 2 ax-mp 
 |-  0hop Fn ~H
4 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
5 4 rgen 
 |-  A. x e. ~H ( 0hop ` x ) = 0h
6 fconstfv 
 |-  ( 0hop : ~H --> { 0h } <-> ( 0hop Fn ~H /\ A. x e. ~H ( 0hop ` x ) = 0h ) )
7 3 5 6 mpbir2an 
 |-  0hop : ~H --> { 0h }
8 ax-hv0cl 
 |-  0h e. ~H
9 8 elexi 
 |-  0h e. _V
10 9 fconst2 
 |-  ( 0hop : ~H --> { 0h } <-> 0hop = ( ~H X. { 0h } ) )
11 7 10 mpbi 
 |-  0hop = ( ~H X. { 0h } )
12 df-ch0 
 |-  0H = { 0h }
13 12 xpeq2i 
 |-  ( ~H X. 0H ) = ( ~H X. { 0h } )
14 11 13 eqtr4i 
 |-  0hop = ( ~H X. 0H )