# Metamath Proof Explorer

## Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ho0.1 𝑇 : ℋ ⟶ ℋ
Assertion ho01i ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ 𝑇 = 0hop )

### Proof

Step Hyp Ref Expression
1 ho0.1 𝑇 : ℋ ⟶ ℋ
2 ffn ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
3 1 2 ax-mp 𝑇 Fn ℋ
4 ax-hv0cl 0 ∈ ℋ
5 4 elexi 0 ∈ V
6 5 fconst ( ℋ × { 0 } ) : ℋ ⟶ { 0 }
7 ffn ( ( ℋ × { 0 } ) : ℋ ⟶ { 0 } → ( ℋ × { 0 } ) Fn ℋ )
8 6 7 ax-mp ( ℋ × { 0 } ) Fn ℋ
9 eqfnfv ( ( 𝑇 Fn ℋ ∧ ( ℋ × { 0 } ) Fn ℋ ) → ( 𝑇 = ( ℋ × { 0 } ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) )
10 3 8 9 mp2an ( 𝑇 = ( ℋ × { 0 } ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( ( ℋ × { 0 } ) ‘ 𝑥 ) )
11 df0op2 0hop = ( ℋ × 0 )
12 df-ch0 0 = { 0 }
13 12 xpeq2i ( ℋ × 0 ) = ( ℋ × { 0 } )
14 11 13 eqtri 0hop = ( ℋ × { 0 } )
15 14 eqeq2i ( 𝑇 = 0hop𝑇 = ( ℋ × { 0 } ) )
16 1 ffvelrni ( 𝑥 ∈ ℋ → ( 𝑇𝑥 ) ∈ ℋ )
17 hial0 ( ( 𝑇𝑥 ) ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇𝑥 ) = 0 ) )
18 16 17 syl ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇𝑥 ) = 0 ) )
19 5 fvconst2 ( 𝑥 ∈ ℋ → ( ( ℋ × { 0 } ) ‘ 𝑥 ) = 0 )
20 19 eqeq2d ( 𝑥 ∈ ℋ → ( ( 𝑇𝑥 ) = ( ( ℋ × { 0 } ) ‘ 𝑥 ) ↔ ( 𝑇𝑥 ) = 0 ) )
21 18 20 bitr4d ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇𝑥 ) = ( ( ℋ × { 0 } ) ‘ 𝑥 ) ) )
22 21 ralbiia ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ ∀ 𝑥 ∈ ℋ ( 𝑇𝑥 ) = ( ( ℋ × { 0 } ) ‘ 𝑥 ) )
23 10 15 22 3bitr4ri ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = 0 ↔ 𝑇 = 0hop )