Theorem hdmap14lem1

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

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

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1.h	|- H = ( LHyp ` K )
2		hdmap14lem1.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap14lem1.v	|- V = ( Base ` U )
4		hdmap14lem1.t	|- .x. = ( .s ` U )
5		hdmap14lem3.o	|- .0. = ( 0g ` U )
6		hdmap14lem1.r	|- R = ( Scalar ` U )
7		hdmap14lem1.b	|- B = ( Base ` R )
8		hdmap14lem1.z	|- Z = ( 0g ` R )
9		hdmap14lem1.c	|- C = ( ( LCDual ` K ) ` W )
10		hdmap14lem2.e	|- .xb = ( .s ` C )
11		hdmap14lem1.l	|- L = ( LSpan ` C )
12		hdmap14lem2.p	|- P = ( Scalar ` C )
13		hdmap14lem2.a	|- A = ( Base ` P )
14		hdmap14lem2.q	|- Q = ( 0g ` P )
15		hdmap14lem1.s	|- S = ( ( HDMap ` K ) ` W )
16		hdmap14lem1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
17		hdmap14lem3.x	|- ( ph -> X e. ( V \ { .0. } ) )
18		hdmap14lem1.f	|- ( ph -> F e. ( B \ { Z } ) )
19	17	eldifad	|- ( ph -> X e. V )
20	18	eldifad	|- ( ph -> F e. B )
21		eldifsni	|- ( F e. ( B \ { Z } ) -> F =/= Z )
22	18 21	syl	|- ( ph -> F =/= Z )
23	1 2 3 4 6 7 9 10 11 12 13 15 16 19 20 8 22	hdmap14lem1a	|- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )