This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) >. )