Theorem hdmaplna1

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

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

Proof

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