Theorem dvaplusg

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

	Ref	Expression
Hypotheses	dvafplus.h	|- H = ( LHyp ` K )
	dvafplus.t	|- T = ( ( LTrn ` K ) ` W )
	dvafplus.e	|- E = ( ( TEndo ` K ) ` W )
	dvafplus.u	|- U = ( ( DVecA ` K ) ` W )
	dvafplus.f	|- F = ( Scalar ` U )
	dvafplus.p	|- .+ = ( +g ` F )
Assertion	dvaplusg	|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E ) ) -> ( R .+ S ) = ( f e. T |-> ( ( R ` f ) o. ( S ` f ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvafplus.h	|- H = ( LHyp ` K )
2		dvafplus.t	|- T = ( ( LTrn ` K ) ` W )
3		dvafplus.e	|- E = ( ( TEndo ` K ) ` W )
4		dvafplus.u	|- U = ( ( DVecA ` K ) ` W )
5		dvafplus.f	|- F = ( Scalar ` U )
6		dvafplus.p	|- .+ = ( +g ` F )
7	1 2 3 4 5 6	dvafplusg	|- ( ( K e. V /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) )
8	7	oveqd	|- ( ( K e. V /\ W e. H ) -> ( R .+ S ) = ( R ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) S ) )
9		eqid	|- ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) = ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) )
10	9 2	tendopl	|- ( ( R e. E /\ S e. E ) -> ( R ( s e. E , t e. E |-> ( g e. T |-> ( ( s ` g ) o. ( t ` g ) ) ) ) S ) = ( f e. T |-> ( ( R ` f ) o. ( S ` f ) ) ) )
11	8 10	sylan9eq	|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E ) ) -> ( R .+ S ) = ( f e. T |-> ( ( R ` f ) o. ( S ` f ) ) ) )