Theorem hdmap14lem1a

Description: Prior to part 14 in Baer p. 49, line 25. (Contributed by NM, 31-May-2015)

	Ref	Expression
Hypotheses	hdmap14lem1a.h	|- H = ( LHyp ` K )
	hdmap14lem1a.u	|- U = ( ( DVecH ` K ) ` W )
	hdmap14lem1a.v	|- V = ( Base ` U )
	hdmap14lem1a.t	|- .x. = ( .s ` U )
	hdmap14lem1a.r	|- R = ( Scalar ` U )
	hdmap14lem1a.b	|- B = ( Base ` R )
	hdmap14lem1a.c	|- C = ( ( LCDual ` K ) ` W )
	hdmap14lem2a.e	|- .xb = ( .s ` C )
	hdmap14lem1a.l	|- L = ( LSpan ` C )
	hdmap14lem2a.p	|- P = ( Scalar ` C )
	hdmap14lem2a.a	|- A = ( Base ` P )
	hdmap14lem1a.s	|- S = ( ( HDMap ` K ) ` W )
	hdmap14lem1a.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmap14lem3a.x	|- ( ph -> X e. V )
	hdmap14lem1a.f	|- ( ph -> F e. B )
	hdmap14lem1a.z	|- .0. = ( 0g ` R )
	hdmap14lem1a.fn	|- ( ph -> F =/= .0. )
Assertion	hdmap14lem1a	|- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1a.h	|- H = ( LHyp ` K )
2		hdmap14lem1a.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap14lem1a.v	|- V = ( Base ` U )
4		hdmap14lem1a.t	|- .x. = ( .s ` U )
5		hdmap14lem1a.r	|- R = ( Scalar ` U )
6		hdmap14lem1a.b	|- B = ( Base ` R )
7		hdmap14lem1a.c	|- C = ( ( LCDual ` K ) ` W )
8		hdmap14lem2a.e	|- .xb = ( .s ` C )
9		hdmap14lem1a.l	|- L = ( LSpan ` C )
10		hdmap14lem2a.p	|- P = ( Scalar ` C )
11		hdmap14lem2a.a	|- A = ( Base ` P )
12		hdmap14lem1a.s	|- S = ( ( HDMap ` K ) ` W )
13		hdmap14lem1a.k	|- ( ph -> ( K e. HL /\ W e. H ) )
14		hdmap14lem3a.x	|- ( ph -> X e. V )
15		hdmap14lem1a.f	|- ( ph -> F e. B )
16		hdmap14lem1a.z	|- .0. = ( 0g ` R )
17		hdmap14lem1a.fn	|- ( ph -> F =/= .0. )
18	1 2 13	dvhlvec	|- ( ph -> U e. LVec )
19		eqid	|- ( LSpan ` U ) = ( LSpan ` U )
20	3 5 4 6 16 19	lspsnvs	|- ( ( U e. LVec /\ ( F e. B /\ F =/= .0. ) /\ X e. V ) -> ( ( LSpan ` U ) ` { ( F .x. X ) } ) = ( ( LSpan ` U ) ` { X } ) )
21	18 15 17 14 20	syl121anc	|- ( ph -> ( ( LSpan ` U ) ` { ( F .x. X ) } ) = ( ( LSpan ` U ) ` { X } ) )
22	21	fveq2d	|- ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { ( F .x. X ) } ) ) = ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { X } ) ) )
23		eqid	|- ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
24	1 2 13	dvhlmod	|- ( ph -> U e. LMod )
25	3 5 4 6	lmodvscl	|- ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
26	24 15 14 25	syl3anc	|- ( ph -> ( F .x. X ) e. V )
27	1 2 3 19 7 9 23 12 13 26	hdmap10	|- ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { ( F .x. X ) } ) ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
28	1 2 3 19 7 9 23 12 13 14	hdmap10	|- ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { X } ) ) = ( L ` { ( S ` X ) } ) )
29	22 27 28	3eqtr3rd	|- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )