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

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 ( 𝐻 ⊆ ℋ → ( 𝐻 ∈ Sℋ ↔ ( 0ℎ ∈ 𝐻 ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ) )

Proof

Step Hyp Ref Expression
1 issh2 ⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) )
2 anass ⊢ ( ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ↔ ( 𝐻 ⊆ ℋ ∧ ( 0ℎ ∈ 𝐻 ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ) )
3 2 baib ⊢ ( 𝐻 ⊆ ℋ → ( ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ↔ ( 0ℎ ∈ 𝐻 ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ) )
4 1 3 bitrid ⊢ ( 𝐻 ⊆ ℋ → ( 𝐻 ∈ Sℋ ↔ ( 0ℎ ∈ 𝐻 ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ) )