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