dvaplusgv

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

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	dvaplusg	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E ) ) -> ( R .+ S ) = ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) )
8	7	fveq1d	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E ) ) -> ( ( R .+ S ) ` G ) = ( ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) ` G ) )
9	8	3adantr3	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E /\ G e. T ) ) -> ( ( R .+ S ) ` G ) = ( ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) ` G ) )
10		simpr3	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E /\ G e. T ) ) -> G e. T )
11		fveq2	\|- ( f = G -> ( R ` f ) = ( R ` G ) )
12		fveq2	\|- ( f = G -> ( S ` f ) = ( S ` G ) )
13	11 12	coeq12d	\|- ( f = G -> ( ( R ` f ) o. ( S ` f ) ) = ( ( R ` G ) o. ( S ` G ) ) )
14		eqid	\|- ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) = ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) )
15		fvex	\|- ( R ` G ) e. _V
16		fvex	\|- ( S ` G ) e. _V
17	15 16	coex	\|- ( ( R ` G ) o. ( S ` G ) ) e. _V
18	13 14 17	fvmpt	\|- ( G e. T -> ( ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) ` G ) = ( ( R ` G ) o. ( S ` G ) ) )
19	10 18	syl	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E /\ G e. T ) ) -> ( ( f e. T \|-> ( ( R ` f ) o. ( S ` f ) ) ) ` G ) = ( ( R ` G ) o. ( S ` G ) ) )
20	9 19	eqtrd	\|- ( ( ( K e. V /\ W e. H ) /\ ( R e. E /\ S e. E /\ G e. T ) ) -> ( ( R .+ S ) ` G ) = ( ( R ` G ) o. ( S ` G ) ) )

Metamath Proof Explorer