Metamath Proof Explorer


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 syl5bir
 |-  ( T : ~H --> ~H -> ( T = (/) -> ~H = (/) ) )
9 2 8 mtoi
 |-  ( T : ~H --> ~H -> -. T = (/) )