Theorem lcdvsval

Description: Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvsval.h	|- H = ( LHyp ` K )
	lcdvsval.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvsval.v	|- V = ( Base ` U )
	lcdvsval.s	|- S = ( Scalar ` U )
	lcdvsval.r	|- R = ( Base ` S )
	lcdvsval.t	|- .x. = ( .r ` S )
	lcdvsval.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvsval.f	|- F = ( Base ` C )
	lcdvsval.m	|- .xb = ( .s ` C )
	lcdvsval.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdvsval.x	|- ( ph -> X e. R )
	lcdvsval.g	|- ( ph -> G e. F )
	lcdvsval.a	|- ( ph -> A e. V )
Assertion	lcdvsval	|- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .x. X ) )

Proof

Step	Hyp	Ref	Expression
1		lcdvsval.h	|- H = ( LHyp ` K )
2		lcdvsval.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdvsval.v	|- V = ( Base ` U )
4		lcdvsval.s	|- S = ( Scalar ` U )
5		lcdvsval.r	|- R = ( Base ` S )
6		lcdvsval.t	|- .x. = ( .r ` S )
7		lcdvsval.c	|- C = ( ( LCDual ` K ) ` W )
8		lcdvsval.f	|- F = ( Base ` C )
9		lcdvsval.m	|- .xb = ( .s ` C )
10		lcdvsval.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		lcdvsval.x	|- ( ph -> X e. R )
12		lcdvsval.g	|- ( ph -> G e. F )
13		lcdvsval.a	|- ( ph -> A e. V )
14		eqid	|- ( LDual ` U ) = ( LDual ` U )
15		eqid	|- ( .s ` ( LDual ` U ) ) = ( .s ` ( LDual ` U ) )
16	1 2 14 15 7 9 10	lcdvs	|- ( ph -> .xb = ( .s ` ( LDual ` U ) ) )
17	16	oveqd	|- ( ph -> ( X .xb G ) = ( X ( .s ` ( LDual ` U ) ) G ) )
18	17	fveq1d	|- ( ph -> ( ( X .xb G ) ` A ) = ( ( X ( .s ` ( LDual ` U ) ) G ) ` A ) )
19		eqid	|- ( LFnl ` U ) = ( LFnl ` U )
20	1 2 10	dvhlmod	|- ( ph -> U e. LMod )
21	1 7 8 2 19 10 12	lcdvbaselfl	|- ( ph -> G e. ( LFnl ` U ) )
22	19 3 4 5 6 14 15 20 11 21 13	ldualvsval	|- ( ph -> ( ( X ( .s ` ( LDual ` U ) ) G ) ` A ) = ( ( G ` A ) .x. X ) )
23	18 22	eqtrd	|- ( ph -> ( ( X .xb G ) ` A ) = ( ( G ` A ) .x. X ) )