This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
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 )