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 )