Theorem dvhopvadd2

Description: The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd and/or dvhfplusr . (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dvhopvadd2.h	|- H = ( LHyp ` K )
	dvhopvadd2.t	|- T = ( ( LTrn ` K ) ` W )
	dvhopvadd2.e	|- E = ( ( TEndo ` K ) ` W )
	dvhopvadd2.p	|- .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
	dvhopvadd2.u	|- U = ( ( DVecH ` K ) ` W )
	dvhopvadd2.s	|- .+b = ( +g ` U )
Assertion	dvhopvadd2	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q .+ R ) >. )

Proof

Step	Hyp	Ref	Expression
1		dvhopvadd2.h	|- H = ( LHyp ` K )
2		dvhopvadd2.t	|- T = ( ( LTrn ` K ) ` W )
3		dvhopvadd2.e	|- E = ( ( TEndo ` K ) ` W )
4		dvhopvadd2.p	|- .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
5		dvhopvadd2.u	|- U = ( ( DVecH ` K ) ` W )
6		dvhopvadd2.s	|- .+b = ( +g ` U )
7		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
8		eqid	|- ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
9	1 2 3 5 7 6 8	dvhopvadd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q ( +g ` ( Scalar ` U ) ) R ) >. )
10	1 2 3 5 7 4 8	dvhfplusr	|- ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = .+ )
11	10	3ad2ant1	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( +g ` ( Scalar ` U ) ) = .+ )
12	11	oveqd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( Q ( +g ` ( Scalar ` U ) ) R ) = ( Q .+ R ) )
13	12	opeq2d	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> <. ( F o. G ) , ( Q ( +g ` ( Scalar ` U ) ) R ) >. = <. ( F o. G ) , ( Q .+ R ) >. )
14	9 13	eqtrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q .+ R ) >. )