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 )