Metamath Proof Explorer

Theorem dvavsca

Description: Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013)

Ref Expression
Hypotheses dvafvsca.h 
|- H = ( LHyp ` K )
dvafvsca.t 
|- T = ( ( LTrn ` K ) ` W )
dvafvsca.e 
|- E = ( ( TEndo ` K ) ` W )
dvafvsca.u 
|- U = ( ( DVecA ` K ) ` W )
dvafvsca.s 
|- .x. = ( .s ` U )
Assertion dvavsca 
|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T ) ) -> ( R .x. F ) = ( R ` F ) )

Proof

Step Hyp Ref Expression
1 dvafvsca.h 
 |-  H = ( LHyp ` K )
2 dvafvsca.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvafvsca.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvafvsca.u 
 |-  U = ( ( DVecA ` K ) ` W )
5 dvafvsca.s 
 |-  .x. = ( .s ` U )
6 1 2 3 4 5 dvafvsca 
 |-  ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , f e. T |-> ( s ` f ) ) )
7 6 oveqd 
 |-  ( ( K e. V /\ W e. H ) -> ( R .x. F ) = ( R ( s e. E , f e. T |-> ( s ` f ) ) F ) )
8 fveq1 
 |-  ( s = R -> ( s ` f ) = ( R ` f ) )
9 fveq2 
 |-  ( f = F -> ( R ` f ) = ( R ` F ) )
10 eqid 
 |-  ( s e. E , f e. T |-> ( s ` f ) ) = ( s e. E , f e. T |-> ( s ` f ) )
11 fvex 
 |-  ( R ` F ) e. _V
12 8 9 10 11 ovmpo 
 |-  ( ( R e. E /\ F e. T ) -> ( R ( s e. E , f e. T |-> ( s ` f ) ) F ) = ( R ` F ) )
13 7 12 sylan9eq 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ F e. T ) ) -> ( R .x. F ) = ( R ` F ) )