Theorem hhssnvt

Description: Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhssnvt.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
Assertion	hhssnvt	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to W\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		hhssnvt.1	$$⊢W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩$$
2		xpeq1	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to H\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times H$$
3		xpeq2	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)$$
4	2 3	eqtrd	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to H\times H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)$$
5	4	reseq2d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)}={{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}$$
6		xpeq2	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to ℂ\times H=ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)$$
7	6	reseq2d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}={{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}$$
8	5 7	opeq12d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to ⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩=⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩$$
9		reseq2	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {{norm}_{ℎ}\upharpoonright }_H={{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}$$
10	8 9	opeq12d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to ⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(H\times H\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times H\right)}⟩,{{norm}_{ℎ}\upharpoonright }_H⟩=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩$$
11	1 10	syl5eq	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to W=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩$$
12	11	eleq1d	$$⊢H=if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left(W\in \mathrm{NrmCVec}\leftrightarrow ⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩\in \mathrm{NrmCVec}\right)$$
13		eqid	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩=⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩$$
14		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
15	14	elimel	$$⊢if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
16	13 15	hhssnv	$$⊢⟨⟨{{+}_{ℎ}\upharpoonright }_{\left(if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)},{{\cdot }_{ℎ}\upharpoonright }_{\left(ℂ\times if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)}⟩,{{norm}_{ℎ}\upharpoonright }_{if\left(H\in {\mathbf{S}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)}⟩\in \mathrm{NrmCVec}$$
17	12 16	dedth	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to W\in \mathrm{NrmCVec}$$