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

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 ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ( +ℎ “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( ·ℎ “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )

Proof

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