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 ⊢ T : ℋ ⟶ ℋ
Assertion ho02i ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ T = 0 hop

Proof

Step Hyp Ref Expression
1 ho0.1 ⊢ T : ℋ ⟶ ℋ
2 ralcom ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ ∀ y ∈ ℋ ∀ x ∈ ℋ x ⋅ ih T ⁡ y = 0
3 1 ffvelcdmi ⊢ y ∈ ℋ → T ⁡ y ∈ ℋ
4 hial02 ⊢ T ⁡ y ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ T ⁡ y = 0 ℎ
5 hial0 ⊢ T ⁡ y ∈ ℋ → ∀ x ∈ ℋ T ⁡ y ⋅ ih x = 0 ↔ T ⁡ y = 0 ℎ
6 4 5 bitr4d ⊢ T ⁡ y ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ ∀ x ∈ ℋ T ⁡ y ⋅ ih x = 0
7 3 6 syl ⊢ y ∈ ℋ → ∀ x ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ ∀ x ∈ ℋ T ⁡ y ⋅ ih x = 0
8 7 ralbiia ⊢ ∀ y ∈ ℋ ∀ x ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ ∀ y ∈ ℋ ∀ x ∈ ℋ T ⁡ y ⋅ ih x = 0
9 1 ho01i ⊢ ∀ y ∈ ℋ ∀ x ∈ ℋ T ⁡ y ⋅ ih x = 0 ↔ T = 0 hop
10 2 8 9 3bitri ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = 0 ↔ T = 0 hop