Metamath Proof Explorer


Theorem dvavadd

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

Ref Expression
Hypotheses dvafvadd.h
|- H = ( LHyp ` K )
dvafvadd.t
|- T = ( ( LTrn ` K ) ` W )
dvafvadd.u
|- U = ( ( DVecA ` K ) ` W )
dvafvadd.v
|- .+ = ( +g ` U )
Assertion dvavadd
|- ( ( ( K e. V /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( F .+ G ) = ( F o. G ) )

Proof

Step Hyp Ref Expression
1 dvafvadd.h
 |-  H = ( LHyp ` K )
2 dvafvadd.t
 |-  T = ( ( LTrn ` K ) ` W )
3 dvafvadd.u
 |-  U = ( ( DVecA ` K ) ` W )
4 dvafvadd.v
 |-  .+ = ( +g ` U )
5 1 2 3 4 dvafvadd
 |-  ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )
6 5 oveqd
 |-  ( ( K e. V /\ W e. H ) -> ( F .+ G ) = ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) )
7 coexg
 |-  ( ( F e. T /\ G e. T ) -> ( F o. G ) e. _V )
8 coeq1
 |-  ( f = F -> ( f o. g ) = ( F o. g ) )
9 coeq2
 |-  ( g = G -> ( F o. g ) = ( F o. G ) )
10 eqid
 |-  ( f e. T , g e. T |-> ( f o. g ) ) = ( f e. T , g e. T |-> ( f o. g ) )
11 8 9 10 ovmpog
 |-  ( ( F e. T /\ G e. T /\ ( F o. G ) e. _V ) -> ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) = ( F o. G ) )
12 7 11 mpd3an3
 |-  ( ( F e. T /\ G e. T ) -> ( F ( f e. T , g e. T |-> ( f o. g ) ) G ) = ( F o. G ) )
13 6 12 sylan9eq
 |-  ( ( ( K e. V /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( F .+ G ) = ( F o. G ) )