Theorem hdmapglnm2

Description: g-linear property of second (inner product) argument. Line 19 in Holland95 p. 14. (Contributed by NM, 10-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmapglnm2.h	|- H = ( LHyp ` K )
2		hdmapglnm2.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapglnm2.v	|- V = ( Base ` U )
4		hdmapglnm2.t	|- .x. = ( .s ` U )
5		hdmapglnm2.r	|- R = ( Scalar ` U )
6		hdmapglnm2.b	|- B = ( Base ` R )
7		hdmapglnm2.m	|- .X. = ( .r ` R )
8		hdmapglnm2.s	|- S = ( ( HDMap ` K ) ` W )
9		hdmapglnm2.g	|- G = ( ( HGMap ` K ) ` W )
10		hdmapglnm2.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		hdmapglnm2.x	|- ( ph -> X e. V )
12		hdmapglnm2.y	|- ( ph -> Y e. V )
13		hdmapglnm2.z	|- ( ph -> A e. B )
14		eqid	|- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
15		eqid	|- ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
16	1 2 3 4 5 6 14 15 8 9 10 12 13	hgmapvs	|- ( ph -> ( S ` ( A .x. Y ) ) = ( ( G ` A ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) )
17	16	fveq1d	|- ( ph -> ( ( S ` ( A .x. Y ) ) ` X ) = ( ( ( G ` A ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) ` X ) )
18		eqid	|- ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
19	1 2 5 6 9 10 13	hgmapcl	|- ( ph -> ( G ` A ) e. B )
20	1 2 3 14 18 8 10 12	hdmapcl	|- ( ph -> ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
21	1 2 3 5 6 7 14 18 15 10 19 20 11	lcdvsval	|- ( ph -> ( ( ( G ` A ) ( .s ` ( ( LCDual ` K ) ` W ) ) ( S ` Y ) ) ` X ) = ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) )
22	17 21	eqtrd	|- ( ph -> ( ( S ` ( A .x. Y ) ) ` X ) = ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) )