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

Metamath Proof Explorer

Theorem hhsssh2

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhsssh2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhsssh2 ( 𝐻 ∈ Sℋ ↔ ( 𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ ) )

Proof

Step Hyp Ref Expression
1 hhsssh2.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3 2 1 hhsssh ⊢ ( 𝐻 ∈ Sℋ ↔ ( 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∧ 𝐻 ⊆ ℋ ) )
4 resss ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ
5 resss ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ
6 resss ⊢ ( normℎ ↾ 𝐻 ) ⊆ normℎ
7 4 5 6 3pm3.2i ⊢ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ )
8 2 hhnv ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
9 2 hhva ⊢ +ℎ = ( +𝑣 ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
10 1 hhssva ⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +𝑣 ‘ 𝑊 )
11 2 hhsm ⊢ ·ℎ = ( ·𝑠OLD ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
12 1 hhsssm ⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·𝑠OLD ‘ 𝑊 )
13 2 hhnm ⊢ normℎ = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
14 1 hhssnm ⊢ ( normℎ ↾ 𝐻 ) = ( normCV ‘ 𝑊 )
15 eqid ⊢ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
16 9 10 11 12 13 14 15 isssp ⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec → ( 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ ) ) ) )
17 8 16 ax-mp ⊢ ( 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +ℎ ∧ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·ℎ ∧ ( normℎ ↾ 𝐻 ) ⊆ normℎ ) ) )
18 7 17 mpbiran2 ⊢ ( 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ↔ 𝑊 ∈ NrmCVec )
19 18 anbi1i ⊢ ( ( 𝑊 ∈ ( SubSp ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) ∧ 𝐻 ⊆ ℋ ) ↔ ( 𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ ) )
20 3 19 bitri ⊢ ( 𝐻 ∈ Sℋ ↔ ( 𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ ) )