Theorem hlhillvec

Description: The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

	Ref	Expression
Hypotheses	hlhillvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hlhillvec	$$⊢\phi \to U\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		hlhillvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
3		hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
4		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5	1 4 3	dvhlvec	$$⊢\phi \to \mathrm{DVecH}\left(K\right)\left(W\right)\in \mathrm{LVec}$$
6		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
7		eqid	$$⊢{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
8	1 2 3 4 7	hlhilbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\mathrm{Base}}_U$$
9		eqid	$$⊢\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)=\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)$$
10		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
11		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
13	1 4 9 2 10 3 12	hlhilsbase2	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
14		eqid	$$⊢{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
15	1 2 3 4 14	hlhilplus	$$⊢\phi \to {+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={+}_U$$
16	15	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}\right)\right)\to x{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}y=x{+}_{U}y$$
17		eqid	$$⊢{+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
18	1 4 9 2 10 3 17	hlhilsplus2	$$⊢\phi \to {+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={+}_{\mathrm{Scalar}\left(U\right)}$$
19	18	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}\right)\right)\to x{+}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}y=x{+}_{\mathrm{Scalar}\left(U\right)}y$$
20		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}$$
21	1 4 9 2 10 3 20	hlhilsmul2	$$⊢\phi \to {\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}={\cdot }_{\mathrm{Scalar}\left(U\right)}$$
22	21	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}\right)\right)\to x{\cdot }_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}y=x{\cdot }_{\mathrm{Scalar}\left(U\right)}y$$
23		eqid	$$⊢{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
24	1 4 23 2 3	hlhilvsca	$$⊢\phi \to {\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\cdot }_U$$
25	24	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{DVecH}\left(K\right)\left(W\right)\right)}\wedge y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}\right)\right)\to x{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}y=x{\cdot }_{U}y$$
26	6 8 9 10 11 13 16 19 22 25	lvecprop2d	$$⊢\phi \to \left(\mathrm{DVecH}\left(K\right)\left(W\right)\in \mathrm{LVec}\leftrightarrow U\in \mathrm{LVec}\right)$$
27	5 26	mpbid	$$⊢\phi \to U\in \mathrm{LVec}$$