Theorem hladdid

Description: Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hladdid.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	hladdid.2	$$⊢G={+}_v\left(U\right)$$
	hladdid.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
Assertion	hladdid	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge A\in X\right)\to AGZ=A$$

Proof

Step	Hyp	Ref	Expression
1		hladdid.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		hladdid.2	$$⊢G={+}_v\left(U\right)$$
3		hladdid.5	$$⊢Z=0_{\mathrm{vec}}\left(U\right)$$
4		hlnv	$$⊢U\in {CHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$
5	1 2 3	nv0rid	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\right)\to AGZ=A$$
6	4 5	sylan	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge A\in X\right)\to AGZ=A$$