Theorem dvhvadd

Description: The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014) (Revised by Mario Carneiro, 23-Jun-2014)

	Ref	Expression
Hypotheses	dvhvadd.h	|- H = ( LHyp ` K )
	dvhvadd.t	|- T = ( ( LTrn ` K ) ` W )
	dvhvadd.e	|- E = ( ( TEndo ` K ) ` W )
	dvhvadd.u	|- U = ( ( DVecH ` K ) ` W )
	dvhvadd.f	|- D = ( Scalar ` U )
	dvhvadd.s	|- .+ = ( +g ` U )
	dvhvadd.p	|- .+^ = ( +g ` D )
Assertion	dvhvadd	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )

Proof

Step	Hyp	Ref	Expression
1		dvhvadd.h	|- H = ( LHyp ` K )
2		dvhvadd.t	|- T = ( ( LTrn ` K ) ` W )
3		dvhvadd.e	|- E = ( ( TEndo ` K ) ` W )
4		dvhvadd.u	|- U = ( ( DVecH ` K ) ` W )
5		dvhvadd.f	|- D = ( Scalar ` U )
6		dvhvadd.s	|- .+ = ( +g ` U )
7		dvhvadd.p	|- .+^ = ( +g ` D )
8		eqid	|- ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. )
9	1 2 3 4 5 7 8 6	dvhfvadd	|- ( ( K e. HL /\ W e. H ) -> .+ = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) )
10	9	oveqd	|- ( ( K e. HL /\ W e. H ) -> ( F .+ G ) = ( F ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) G ) )
11	8	dvhvaddval	|- ( ( F e. ( T X. E ) /\ G e. ( T X. E ) ) -> ( F ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
12	10 11	sylan9eq	|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )