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