# Metamath Proof Explorer

## Theorem ho02i

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

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

### Proof

Step Hyp Ref Expression
1 ho0.1 𝑇 : ℋ ⟶ ℋ
2 ralcom ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 )
3 1 ffvelrni ( 𝑦 ∈ ℋ → ( 𝑇𝑦 ) ∈ ℋ )
4 hial02 ( ( 𝑇𝑦 ) ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ ( 𝑇𝑦 ) = 0 ) )
5 hial0 ( ( 𝑇𝑦 ) ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = 0 ↔ ( 𝑇𝑦 ) = 0 ) )
6 4 5 bitr4d ( ( 𝑇𝑦 ) ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = 0 ) )
7 3 6 syl ( 𝑦 ∈ ℋ → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = 0 ) )
8 7 ralbiia ( ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = 0 )
9 1 ho01i ( ∀ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑇𝑦 ) ·ih 𝑥 ) = 0 ↔ 𝑇 = 0hop )
10 2 8 9 3bitri ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = 0 ↔ 𝑇 = 0hop )