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 = ( LHyp ` K )
	hlhil0.l	|- L = ( ( DVecH ` K ) ` W )
	hlhil0.u	|- U = ( ( HLHil ` K ) ` W )
	hlhil0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhillsm.a	|- .(+) = ( LSSum ` L )
Assertion	hlhillsm	|- ( ph -> .(+) = ( LSSum ` U ) )

Proof

Step	Hyp	Ref	Expression
1		hlhil0.h	|- H = ( LHyp ` K )
2		hlhil0.l	|- L = ( ( DVecH ` K ) ` W )
3		hlhil0.u	|- U = ( ( HLHil ` K ) ` W )
4		hlhil0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
5		hlhillsm.a	|- .(+) = ( LSSum ` L )
6		eqidd	|- ( ph -> ( Base ` L ) = ( Base ` L ) )
7		eqid	|- ( Base ` L ) = ( Base ` L )
8	1 3 4 2 7	hlhilbase	|- ( ph -> ( Base ` L ) = ( Base ` U ) )
9		eqid	|- ( +g ` L ) = ( +g ` L )
10	1 3 4 2 9	hlhilplus	|- ( ph -> ( +g ` L ) = ( +g ` U ) )
11	10	oveqdr	|- ( ( ph /\ ( x e. ( Base ` L ) /\ y e. ( Base ` L ) ) ) -> ( x ( +g ` L ) y ) = ( x ( +g ` U ) y ) )
12	2	fvexi	|- L e. _V
13	12	a1i	|- ( ph -> L e. _V )
14	3	fvexi	|- U e. _V
15	14	a1i	|- ( ph -> U e. _V )
16	6 8 11 13 15	lsmpropd	|- ( ph -> ( LSSum ` L ) = ( LSSum ` U ) )
17	5 16	syl5eq	|- ( ph -> .(+) = ( LSSum ` U ) )