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

Metamath Proof Explorer

Theorem dvhopvadd2

Description: The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd and/or dvhfplusr . (Contributed by NM, 26-Sep-2014)

		Ref	Expression
	Hypotheses	dvhopvadd2.h	\|- H = ( LHyp ` K )
		dvhopvadd2.t	\|- T = ( ( LTrn ` K ) ` W )
		dvhopvadd2.e	\|- E = ( ( TEndo ` K ) ` W )
		dvhopvadd2.p	\|- .+ = ( s e. E , t e. E \|-> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) )
		dvhopvadd2.u	\|- U = ( ( DVecH ` K ) ` W )
		dvhopvadd2.s	\|- .+b = ( +g ` U )
	Assertion	dvhopvadd2	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q .+ R ) >. )

Proof

Step	Hyp	Ref	Expression
1		dvhopvadd2.h	\|- H = ( LHyp ` K )
2		dvhopvadd2.t	\|- T = ( ( LTrn ` K ) ` W )
3		dvhopvadd2.e	\|- E = ( ( TEndo ` K ) ` W )
4		dvhopvadd2.p	\|- .+ = ( s e. E , t e. E \|-> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) )
5		dvhopvadd2.u	\|- U = ( ( DVecH ` K ) ` W )
6		dvhopvadd2.s	\|- .+b = ( +g ` U )
7		eqid	\|- ( Scalar ` U ) = ( Scalar ` U )
8		eqid	\|- ( +g ` ( Scalar ` U ) ) = ( +g ` ( Scalar ` U ) )
9	1 2 3 5 7 6 8	dvhopvadd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q ( +g ` ( Scalar ` U ) ) R ) >. )
10	1 2 3 5 7 4 8	dvhfplusr	\|- ( ( K e. HL /\ W e. H ) -> ( +g ` ( Scalar ` U ) ) = .+ )
11	10	3ad2ant1	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( +g ` ( Scalar ` U ) ) = .+ )
12	11	oveqd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( Q ( +g ` ( Scalar ` U ) ) R ) = ( Q .+ R ) )
13	12	opeq2d	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> <. ( F o. G ) , ( Q ( +g ` ( Scalar ` U ) ) R ) >. = <. ( F o. G ) , ( Q .+ R ) >. )
14	9 13	eqtrd	\|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ Q e. E ) /\ ( G e. T /\ R e. E ) ) -> ( <. F , Q >. .+b <. G , R >. ) = <. ( F o. G ) , ( Q .+ R ) >. )