Theorem hdmaplna2

Description: Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015)

	Ref	Expression
Hypotheses	hdmaplna2.h	|- H = ( LHyp ` K )
	hdmaplna2.u	|- U = ( ( DVecH ` K ) ` W )
	hdmaplna2.v	|- V = ( Base ` U )
	hdmaplna2.p	|- .+ = ( +g ` U )
	hdmaplna2.r	|- R = ( Scalar ` U )
	hdmaplna2.q	|- .+^ = ( +g ` R )
	hdmaplna2.s	|- S = ( ( HDMap ` K ) ` W )
	hdmaplna2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmaplna2.x	|- ( ph -> X e. V )
	hdmaplna2.y	|- ( ph -> Y e. V )
	hdmaplna2.z	|- ( ph -> Z e. V )
Assertion	hdmaplna2	|- ( ph -> ( ( S ` ( Y .+ Z ) ) ` X ) = ( ( ( S ` Y ) ` X ) .+^ ( ( S ` Z ) ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaplna2.h	|- H = ( LHyp ` K )
2		hdmaplna2.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmaplna2.v	|- V = ( Base ` U )
4		hdmaplna2.p	|- .+ = ( +g ` U )
5		hdmaplna2.r	|- R = ( Scalar ` U )
6		hdmaplna2.q	|- .+^ = ( +g ` R )
7		hdmaplna2.s	|- S = ( ( HDMap ` K ) ` W )
8		hdmaplna2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		hdmaplna2.x	|- ( ph -> X e. V )
10		hdmaplna2.y	|- ( ph -> Y e. V )
11		hdmaplna2.z	|- ( ph -> Z e. V )
12		eqid	|- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
13		eqid	|- ( +g ` ( ( LCDual ` K ) ` W ) ) = ( +g ` ( ( LCDual ` K ) ` W ) )
14	1 2 3 4 12 13 7 8 10 11	hdmapadd	|- ( ph -> ( S ` ( Y .+ Z ) ) = ( ( S ` Y ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( S ` Z ) ) )
15	14	fveq1d	|- ( ph -> ( ( S ` ( Y .+ Z ) ) ` X ) = ( ( ( S ` Y ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( S ` Z ) ) ` X ) )
16		eqid	|- ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
17	1 2 3 12 16 7 8 10	hdmapcl	|- ( ph -> ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
18	1 2 3 12 16 7 8 11	hdmapcl	|- ( ph -> ( S ` Z ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
19	1 2 3 5 6 12 16 13 8 17 18 9	lcdvaddval	|- ( ph -> ( ( ( S ` Y ) ( +g ` ( ( LCDual ` K ) ` W ) ) ( S ` Z ) ) ` X ) = ( ( ( S ` Y ) ` X ) .+^ ( ( S ` Z ) ` X ) ) )
20	15 19	eqtrd	|- ( ph -> ( ( S ` ( Y .+ Z ) ) ` X ) = ( ( ( S ` Y ) ` X ) .+^ ( ( S ` Z ) ` X ) ) )