Theorem hon0

Description: A Hilbert space operator is not empty. (Contributed by NM, 24-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hon0	|- ( T : ~H --> ~H -> -. T = (/) )

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	|- 0h e. ~H
2	1	n0ii	|- -. ~H = (/)
3		fn0	|- ( T Fn (/) <-> T = (/) )
4		ffn	|- ( T : ~H --> ~H -> T Fn ~H )
5		fndmu	|- ( ( T Fn ~H /\ T Fn (/) ) -> ~H = (/) )
6	5	ex	|- ( T Fn ~H -> ( T Fn (/) -> ~H = (/) ) )
7	4 6	syl	|- ( T : ~H --> ~H -> ( T Fn (/) -> ~H = (/) ) )
8	3 7	biimtrrid	|- ( T : ~H --> ~H -> ( T = (/) -> ~H = (/) ) )
9	2 8	mtoi	|- ( T : ~H --> ~H -> -. T = (/) )