Theorem hdmap14lem15

Description: Part of proof of part 14 in Baer p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem12.h	|- H = ( LHyp ` K )
	hdmap14lem12.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap14lem12.v	|- V = ( Base ` U )
	hdmap14lem12.t	|- .x. = ( .s ` U )
	hdmap14lem12.r	|- R = ( Scalar ` U )
	hdmap14lem12.b	|- B = ( Base ` R )
	hdmap14lem12.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap14lem12.e	|- .xb = ( .s ` C )
	hdmap14lem12.s	|- S = ( ( HDMap ` K ) ` W )
	hdmap14lem12.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap14lem12.f	|- ( ph -> F e. B )
Assertion	hdmap14lem15	|- ( ph -> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem12.h	|- H = ( LHyp ` K )
2		hdmap14lem12.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap14lem12.v	|- V = ( Base ` U )
4		hdmap14lem12.t	|- .x. = ( .s ` U )
5		hdmap14lem12.r	|- R = ( Scalar ` U )
6		hdmap14lem12.b	|- B = ( Base ` R )
7		hdmap14lem12.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap14lem12.e	|- .xb = ( .s ` C )
9		hdmap14lem12.s	|- S = ( ( HDMap ` K ) ` W )
10		hdmap14lem12.k	|- ( ph -> ( K e. HL /\ W e. H ) )
11		hdmap14lem12.f	|- ( ph -> F e. B )
12		eqid	|- ( Scalar ` C ) = ( Scalar ` C )
13		eqid	|- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
14	1 2 3 4 5 6 7 8 9 10 11 12 13	hdmap14lem14	|- ( ph -> E! g e. ( Base ` ( Scalar ` C ) ) A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )
15	1 2 5 6 7 12 13 10	lcdsbase	|- ( ph -> ( Base ` ( Scalar ` C ) ) = B )
16		reueq1	|- ( ( Base ` ( Scalar ` C ) ) = B -> ( E! g e. ( Base ` ( Scalar ` C ) ) A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) <-> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
17	15 16	syl	|- ( ph -> ( E! g e. ( Base ` ( Scalar ` C ) ) A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) <-> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) ) )
18	14 17	mpbid	|- ( ph -> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )