Theorem hlhil0

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

	Ref	Expression
Hypotheses	hlhil0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhil0.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhil0.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhil0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhil0.z	$$⊢\underset{\dot{}}{0}=0_L$$
Assertion	hlhil0	$$⊢\phi \to \underset{\dot{}}{0}=0_U$$

Proof

Step	Hyp	Ref	Expression
1		hlhil0.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhil0.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hlhil0.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
4		hlhil0.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
5		hlhil0.z	$$⊢\underset{\dot{}}{0}=0_L$$
6		eqidd	$$⊢\phi \to {\mathrm{Base}}_L={\mathrm{Base}}_L$$
7		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
8	1 3 4 2 7	hlhilbase	$$⊢\phi \to {\mathrm{Base}}_L={\mathrm{Base}}_U$$
9		eqid	$$⊢{+}_L={+}_L$$
10	1 3 4 2 9	hlhilplus	$$⊢\phi \to {+}_L={+}_U$$
11	10	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_L\wedge y\in {\mathrm{Base}}_L\right)\right)\to x{+}_{L}y=x{+}_{U}y$$
12	6 8 11	grpidpropd	$$⊢\phi \to 0_L=0_U$$
13	5 12	eqtrid	$$⊢\phi \to \underset{\dot{}}{0}=0_U$$