Theorem hdmapgln2

Description: g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmapgln2.h	|- H = ( LHyp ` K )
2		hdmapgln2.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapgln2.v	|- V = ( Base ` U )
4		hdmapgln2.p	|- .+ = ( +g ` U )
5		hdmapgln2.t	|- .x. = ( .s ` U )
6		hdmapgln2.r	|- R = ( Scalar ` U )
7		hdmapgln2.b	|- B = ( Base ` R )
8		hdmapgln2.q	|- .+^ = ( +g ` R )
9		hdmapgln2.m	|- .X. = ( .r ` R )
10		hdmapgln2.s	|- S = ( ( HDMap ` K ) ` W )
11		hdmapgln2.g	|- G = ( ( HGMap ` K ) ` W )
12		hdmapgln2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
13		hdmapgln2.x	|- ( ph -> X e. V )
14		hdmapgln2.y	|- ( ph -> Y e. V )
15		hdmapgln2.z	|- ( ph -> Z e. V )
16		hdmapgln2.a	|- ( ph -> A e. B )
17	1 2 12	dvhlmod	|- ( ph -> U e. LMod )
18	3 6 5 7	lmodvscl	|- ( ( U e. LMod /\ A e. B /\ Y e. V ) -> ( A .x. Y ) e. V )
19	17 16 14 18	syl3anc	|- ( ph -> ( A .x. Y ) e. V )
20	1 2 3 4 6 8 10 12 13 19 15	hdmaplna2	|- ( ph -> ( ( S ` ( ( A .x. Y ) .+ Z ) ) ` X ) = ( ( ( S ` ( A .x. Y ) ) ` X ) .+^ ( ( S ` Z ) ` X ) ) )
21	1 2 3 5 6 7 9 10 11 12 13 14 16	hdmapglnm2	|- ( ph -> ( ( S ` ( A .x. Y ) ) ` X ) = ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) )
22	21	oveq1d	|- ( ph -> ( ( ( S ` ( A .x. Y ) ) ` X ) .+^ ( ( S ` Z ) ` X ) ) = ( ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) .+^ ( ( S ` Z ) ` X ) ) )
23	20 22	eqtrd	|- ( ph -> ( ( S ` ( ( A .x. Y ) .+ Z ) ) ` X ) = ( ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) .+^ ( ( S ` Z ) ` X ) ) )