Theorem hdmaplns1

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

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

Proof

Step	Hyp	Ref	Expression
1		hdmaplns1.h	|- H = ( LHyp ` K )
2		hdmaplns1.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmaplns1.v	|- V = ( Base ` U )
4		hdmaplns1.m	|- .- = ( -g ` U )
5		hdmaplns1.r	|- R = ( Scalar ` U )
6		hdmaplns1.n	|- N = ( -g ` R )
7		hdmaplns1.s	|- S = ( ( HDMap ` K ) ` W )
8		hdmaplns1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		hdmaplns1.x	|- ( ph -> X e. V )
10		hdmaplns1.y	|- ( ph -> Y e. V )
11		hdmaplns1.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	lflsub	|- ( ( U e. LMod /\ ( S ` Z ) e. ( LFnl ` U ) /\ ( X e. V /\ Y e. V ) ) -> ( ( S ` Z ) ` ( X .- Y ) ) = ( ( ( S ` Z ) ` X ) N ( ( S ` Z ) ` Y ) ) )
19	12 17 9 10 18	syl112anc	|- ( ph -> ( ( S ` Z ) ` ( X .- Y ) ) = ( ( ( S ` Z ) ` X ) N ( ( S ` Z ) ` Y ) ) )