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

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