Theorem hlhilsplus2

Description: Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilsbase.h	|- H = ( LHyp ` K )
	hlhilsbase.l	|- L = ( ( DVecH ` K ) ` W )
	hlhilsbase.s	|- S = ( Scalar ` L )
	hlhilsbase.u	|- U = ( ( HLHil ` K ) ` W )
	hlhilsbase.r	|- R = ( Scalar ` U )
	hlhilsbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhilsplus2.a	|- .+ = ( +g ` S )
Assertion	hlhilsplus2	|- ( ph -> .+ = ( +g ` R ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilsbase.h	|- H = ( LHyp ` K )
2		hlhilsbase.l	|- L = ( ( DVecH ` K ) ` W )
3		hlhilsbase.s	|- S = ( Scalar ` L )
4		hlhilsbase.u	|- U = ( ( HLHil ` K ) ` W )
5		hlhilsbase.r	|- R = ( Scalar ` U )
6		hlhilsbase.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		hlhilsplus2.a	|- .+ = ( +g ` S )
8		eqid	|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
9	1 8 2 3	dvhsca	|- ( ( K e. HL /\ W e. H ) -> S = ( ( EDRing ` K ) ` W ) )
10	6 9	syl	|- ( ph -> S = ( ( EDRing ` K ) ` W ) )
11	10	fveq2d	|- ( ph -> ( +g ` S ) = ( +g ` ( ( EDRing ` K ) ` W ) ) )
12	7 11	syl5eq	|- ( ph -> .+ = ( +g ` ( ( EDRing ` K ) ` W ) ) )
13		eqid	|- ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` ( ( EDRing ` K ) ` W ) )
14	1 8 4 5 6 13	hlhilsplus	|- ( ph -> ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` R ) )
15	12 14	eqtrd	|- ( ph -> .+ = ( +g ` R ) )