Metamath Proof Explorer

Theorem issh

Description: Subspace H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion issh ⊢ H ∈ S ℋ ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 elpw2 ⊢ H ∈ 𝒫 ℋ ↔ H ⊆ ℋ
3 3anass ⊢ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H ↔ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H
4 2 3 anbi12i ⊢ H ∈ 𝒫 ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H
5 eleq2 ⊢ h = H → 0 ℎ ∈ h ↔ 0 ℎ ∈ H
6 id ⊢ h = H → h = H
7 6 sqxpeqd ⊢ h = H → h × h = H × H
8 7 imaeq2d ⊢ h = H → + ℎ h × h = + ℎ H × H
9 8 6 sseq12d ⊢ h = H → + ℎ h × h ⊆ h ↔ + ℎ H × H ⊆ H
10 xpeq2 ⊢ h = H → ℂ × h = ℂ × H
11 10 imaeq2d ⊢ h = H → ⋅ ℎ ℂ × h = ⋅ ℎ ℂ × H
12 11 6 sseq12d ⊢ h = H → ⋅ ℎ ℂ × h ⊆ h ↔ ⋅ ℎ ℂ × H ⊆ H
13 5 9 12 3anbi123d ⊢ h = H → 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h ↔ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H
14 df-sh ⊢ S ℋ = h ∈ 𝒫 ℋ | 0 ℎ ∈ h ∧ + ℎ h × h ⊆ h ∧ ⋅ ℎ ℂ × h ⊆ h
15 13 14 elrab2 ⊢ H ∈ S ℋ ↔ H ∈ 𝒫 ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H
16 anass ⊢ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H
17 4 15 16 3bitr4i ⊢ H ∈ S ℋ ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ + ℎ H × H ⊆ H ∧ ⋅ ℎ ℂ × H ⊆ H