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