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

Metamath Proof Explorer

Theorem dvhopvsca

Description: Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014)

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 dvhopvsca 
|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R .x. <. F , X >. ) = <. ( R ` F ) , ( R o. X ) >. )

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 simpl 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( K e. V /\ W e. H ) )
7 simpr1 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> R e. E )
8 simpr2 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> F e. T )
9 simpr3 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> X e. E )
10 opelxpi 
 |-  ( ( F e. T /\ X e. E ) -> <. F , X >. e. ( T X. E ) )
11 8 9 10 syl2anc 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> <. F , X >. e. ( T X. E ) )
12 1 2 3 4 5 dvhvsca 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ <. F , X >. e. ( T X. E ) ) ) -> ( R .x. <. F , X >. ) = <. ( R ` ( 1st ` <. F , X >. ) ) , ( R o. ( 2nd ` <. F , X >. ) ) >. )
13 6 7 11 12 syl12anc 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R .x. <. F , X >. ) = <. ( R ` ( 1st ` <. F , X >. ) ) , ( R o. ( 2nd ` <. F , X >. ) ) >. )
14 op1stg 
 |-  ( ( F e. T /\ X e. E ) -> ( 1st ` <. F , X >. ) = F )
15 8 9 14 syl2anc 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( 1st ` <. F , X >. ) = F )
16 15 fveq2d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R ` ( 1st ` <. F , X >. ) ) = ( R ` F ) )
17 op2ndg 
 |-  ( ( F e. T /\ X e. E ) -> ( 2nd ` <. F , X >. ) = X )
18 8 9 17 syl2anc 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( 2nd ` <. F , X >. ) = X )
19 18 coeq2d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R o. ( 2nd ` <. F , X >. ) ) = ( R o. X ) )
20 16 19 opeq12d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> <. ( R ` ( 1st ` <. F , X >. ) ) , ( R o. ( 2nd ` <. F , X >. ) ) >. = <. ( R ` F ) , ( R o. X ) >. )
21 13 20 eqtrd 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T /\ X e. E ) ) -> ( R .x. <. F , X >. ) = <. ( R ` F ) , ( R o. X ) >. )