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	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
Assertion	hhsssh2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge H\subseteq \mathscr{H}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhsssh2.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
2		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
3	2 1	hhsssh	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \left(W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\wedge H\subseteq \mathscr{H}\right)$$
4		resss	$$⊢{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\subseteq {+}_{ℎ}$$
5		resss	$$⊢{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}\subseteq {\cdot }_{ℎ}$$
6		resss	$$⊢{{norm}_{ℎ}\upharpoonright }_H\subseteq {norm}_{ℎ}$$
7	4 5 6	3pm3.2i	$$⊢\left({{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\subseteq {+}_{ℎ}\wedge {{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}\subseteq {\cdot }_{ℎ}\wedge {{norm}_{ℎ}\upharpoonright }_H\subseteq {norm}_{ℎ}\right)$$
8	2	hhnv	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
9	2	hhva	$$⊢{+}_{ℎ}={+}_v\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
10	1	hhssva	$$⊢{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={+}_v\left(W\right)$$
11	2	hhsm	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
12	1	hhsssm	$$⊢{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
13	2	hhnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
14	1	hhssnm	$$⊢{{norm}_{ℎ}\upharpoonright }_H={norm}_{CV}\left(W\right)$$
15		eqid	$$⊢\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=\mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
16	9 10 11 12 13 14 15	isssp	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\to \left(W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge \left({{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\subseteq {+}_{ℎ}\wedge {{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}\subseteq {\cdot }_{ℎ}\wedge {{norm}_{ℎ}\upharpoonright }_H\subseteq {norm}_{ℎ}\right)\right)\right)$$
17	8 16	ax-mp	$$⊢W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge \left({{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}\subseteq {+}_{ℎ}\wedge {{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}\subseteq {\cdot }_{ℎ}\wedge {{norm}_{ℎ}\upharpoonright }_H\subseteq {norm}_{ℎ}\right)\right)$$
18	7 17	mpbiran2	$$⊢W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\leftrightarrow W\in \mathrm{NrmCVec}$$
19	18	anbi1i	$$⊢\left(W\in \mathrm{SubSp}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\wedge H\subseteq \mathscr{H}\right)\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge H\subseteq \mathscr{H}\right)$$
20	3 19	bitri	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge H\subseteq \mathscr{H}\right)$$