Theorem hgmapdcl

Description: Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hgmapdcl.h	|- H = ( LHyp ` K )
	hgmapdcl.u	|- U = ( ( DVecH ` K ) ` W )
	hgmapdcl.r	|- R = ( Scalar ` U )
	hgmapdcl.b	|- B = ( Base ` R )
	hgmapdcl.c	|- C = ( ( LCDual ` K ) ` W )
	hgmapdcl.q	|- Q = ( Scalar ` C )
	hgmapdcl.a	|- A = ( Base ` Q )
	hgmapdcl.g	|- G = ( ( HGMap ` K ) ` W )
	hgmapdcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hgmapdcl.f	|- ( ph -> F e. B )
Assertion	hgmapdcl	|- ( ph -> ( G ` F ) e. A )

Proof

Step	Hyp	Ref	Expression
1		hgmapdcl.h	|- H = ( LHyp ` K )
2		hgmapdcl.u	|- U = ( ( DVecH ` K ) ` W )
3		hgmapdcl.r	|- R = ( Scalar ` U )
4		hgmapdcl.b	|- B = ( Base ` R )
5		hgmapdcl.c	|- C = ( ( LCDual ` K ) ` W )
6		hgmapdcl.q	|- Q = ( Scalar ` C )
7		hgmapdcl.a	|- A = ( Base ` Q )
8		hgmapdcl.g	|- G = ( ( HGMap ` K ) ` W )
9		hgmapdcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		hgmapdcl.f	|- ( ph -> F e. B )
11	1 2 3 4 8 9 10	hgmapcl	|- ( ph -> ( G ` F ) e. B )
12	1 2 3 4 5 6 7 9	lcdsbase	|- ( ph -> A = B )
13	11 12	eleqtrrd	|- ( ph -> ( G ` F ) e. A )