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𝐻 ) ∧ ( ( + “ ( 𝐻 × 𝐻 ) ) ⊆ 𝐻 ∧ ( · “ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) )