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 ∈ H x + ℎ y ∈ H ∧ ∀ x ∈ ℂ ∀ y ∈ H x ⋅ ℎ y ∈ H

Proof

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