Theorem hlhillsm

Description: The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-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)$$
	hlhillsm.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(L\right)$$
Assertion	hlhillsm	$$⊢\phi \to \underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$

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		hlhillsm.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(L\right)$$
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	2	fvexi	$$⊢L\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to L\in \mathrm{V}$$
14	3	fvexi	$$⊢U\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to U\in \mathrm{V}$$
16	6 8 11 13 15	lsmpropd	$$⊢\phi \to \mathrm{LSSum}\left(L\right)=\mathrm{LSSum}\left(U\right)$$
17	5 16	syl5eq	$$⊢\phi \to \underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$