Metamath Proof Explorer

Theorem hhsst

Description: A member of SH is a subspace. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	hhsst.1	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
		hhsst.2	⊢ 𝑊 = ⟨ ⟨ ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( norm_ℎ ↾ 𝐻 ) ⟩
	Assertion	hhsst	⊢ ( 𝐻 ∈ S_ℋ → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		hhsst.1	⊢ 𝑈 = ⟨ ⟨ +_ℎ , ·_ℎ ⟩ , norm_ℎ ⟩
2		hhsst.2	⊢ 𝑊 = ⟨ ⟨ ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( norm_ℎ ↾ 𝐻 ) ⟩
3	2	hhssnvt	⊢ ( 𝐻 ∈ S_ℋ → 𝑊 ∈ NrmCVec )
4		resss	⊢ ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +_ℎ
5		resss	⊢ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·_ℎ
6		resss	⊢ ( norm_ℎ ↾ 𝐻 ) ⊆ norm_ℎ
7	4 5 6	3pm3.2i	⊢ ( ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +_ℎ ∧ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·_ℎ ∧ ( norm_ℎ ↾ 𝐻 ) ⊆ norm_ℎ )
8	3 7	jctir	⊢ ( 𝐻 ∈ S_ℋ → ( 𝑊 ∈ NrmCVec ∧ ( ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +_ℎ ∧ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·_ℎ ∧ ( norm_ℎ ↾ 𝐻 ) ⊆ norm_ℎ ) ) )
9	1	hhnv	⊢ 𝑈 ∈ NrmCVec
10	1	hhva	⊢ +_ℎ = ( +_𝑣 ‘ 𝑈 )
11	2	hhssva	⊢ ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +_𝑣 ‘ 𝑊 )
12	1	hhsm	⊢ ·_ℎ = ( ·_𝑠OLD ‘ 𝑈 )
13	2	hhsssm	⊢ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·_𝑠OLD ‘ 𝑊 )
14	1	hhnm	⊢ norm_ℎ = ( norm_CV ‘ 𝑈 )
15	2	hhssnm	⊢ ( norm_ℎ ↾ 𝐻 ) = ( norm_CV ‘ 𝑊 )
16		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
17	10 11 12 13 14 15 16	isssp	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +_ℎ ∧ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·_ℎ ∧ ( norm_ℎ ↾ 𝐻 ) ⊆ norm_ℎ ) ) ) )
18	9 17	ax-mp	⊢ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +_ℎ ↾ ( 𝐻 × 𝐻 ) ) ⊆ +_ℎ ∧ ( ·_ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ ·_ℎ ∧ ( norm_ℎ ↾ 𝐻 ) ⊆ norm_ℎ ) ) )
19	8 18	sylibr	⊢ ( 𝐻 ∈ S_ℋ → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )