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

Metamath Proof Explorer

Theorem dvhvsca

Description: Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013)

Ref Expression
Hypotheses dvhfvsca.h 
|- H = ( LHyp ` K )
dvhfvsca.t 
|- T = ( ( LTrn ` K ) ` W )
dvhfvsca.e 
|- E = ( ( TEndo ` K ) ` W )
dvhfvsca.u 
|- U = ( ( DVecH ` K ) ` W )
dvhfvsca.s 
|- .x. = ( .s ` U )
Assertion dvhvsca 
|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. ( T X. E ) ) ) -> ( R .x. F ) = <. ( R ` ( 1st ` F ) ) , ( R o. ( 2nd ` F ) ) >. )

Proof

Step Hyp Ref Expression
1 dvhfvsca.h 
 |-  H = ( LHyp ` K )
2 dvhfvsca.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhfvsca.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhfvsca.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhfvsca.s 
 |-  .x. = ( .s ` U )
6 1 2 3 4 5 dvhfvsca 
 |-  ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) )
7 6 oveqd 
 |-  ( ( K e. V /\ W e. H ) -> ( R .x. F ) = ( R ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) F ) )
8 eqid 
 |-  ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. )
9 8 dvhvscaval 
 |-  ( ( R e. E /\ F e. ( T X. E ) ) -> ( R ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) F ) = <. ( R ` ( 1st ` F ) ) , ( R o. ( 2nd ` F ) ) >. )
10 7 9 sylan9eq 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. ( T X. E ) ) ) -> ( R .x. F ) = <. ( R ` ( 1st ` F ) ) , ( R o. ( 2nd ` F ) ) >. )