Metamath Proof Explorer

Theorem issh3

Description: Subspace H of a Hilbert space. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

Ref Expression
Assertion issh3 ⊢H⊆ℋ→H∈Sℋ↔0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H

Proof

Step Hyp Ref Expression
1 issh2 ⊢H∈Sℋ↔H⊆ℋ∧0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H
2 anass ⊢H⊆ℋ∧0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H↔H⊆ℋ∧0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H
3 2 baib ⊢H⊆ℋ→H⊆ℋ∧0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H↔0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H
4 1 3 bitrid ⊢H⊆ℋ→H∈Sℋ↔0ℎ∈H∧∀x∈H∀y∈Hx+ℎy∈H∧∀x∈ℂ∀y∈Hx⋅ℎy∈H