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ℎ ∈ 𝐻 ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) ) )