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 = (/) ) |
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 = (/) ) |