Theorem hgmapcl

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

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

Proof

Step	Hyp	Ref	Expression
1		hgmapcl.h	|- H = ( LHyp ` K )
2		hgmapcl.u	|- U = ( ( DVecH ` K ) ` W )
3		hgmapcl.r	|- R = ( Scalar ` U )
4		hgmapcl.b	|- B = ( Base ` R )
5		hgmapcl.g	|- G = ( ( HGMap ` K ) ` W )
6		hgmapcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		hgmapcl.f	|- ( ph -> F e. B )
8		eqid	|- ( Base ` U ) = ( Base ` U )
9		eqid	|- ( .s ` U ) = ( .s ` U )
10		eqid	|- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
11		eqid	|- ( .s ` ( ( LCDual ` K ) ` W ) ) = ( .s ` ( ( LCDual ` K ) ` W ) )
12		eqid	|- ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
13	1 2 8 9 3 4 10 11 12 5 6 7	hgmapval	|- ( ph -> ( G ` F ) = ( iota_ g e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( F ( .s ` U ) x ) ) = ( g ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) )
14	1 2 8 9 3 4 10 11 12 6 7	hdmap14lem15	|- ( ph -> E! g e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( F ( .s ` U ) x ) ) = ( g ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) )
15		riotacl	|- ( E! g e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( F ( .s ` U ) x ) ) = ( g ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) -> ( iota_ g e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( F ( .s ` U ) x ) ) = ( g ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) e. B )
16	14 15	syl	|- ( ph -> ( iota_ g e. B A. x e. ( Base ` U ) ( ( ( HDMap ` K ) ` W ) ` ( F ( .s ` U ) x ) ) = ( g ( .s ` ( ( LCDual ` K ) ` W ) ) ( ( ( HDMap ` K ) ` W ) ` x ) ) ) e. B )
17	13 16	eqeltrd	|- ( ph -> ( G ` F ) e. B )