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 ∧ 𝐻 ⊆ ℋ ) )