Theorem hdmap14lem2N

Description: Prior to part 14 in Baer p. 49, line 25. TODO: fix to include F = Z so it can be used in hdmap14lem10 . (Contributed by NM, 31-May-2015) (New usage is discouraged.)

	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	hdmap14lem2N	|- ( ph -> E. g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` 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	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hdmap14lem1	|- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
20	19	eqcomd	|- ( ph -> ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) )
21		eqid	|- ( Base ` C ) = ( Base ` C )
22	1 9 16	lcdlvec	|- ( ph -> C e. LVec )
23	1 2 16	dvhlmod	|- ( ph -> U e. LMod )
24	18	eldifad	|- ( ph -> F e. B )
25	17	eldifad	|- ( ph -> X e. V )
26	3 6 4 7	lmodvscl	|- ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
27	23 24 25 26	syl3anc	|- ( ph -> ( F .x. X ) e. V )
28	1 2 3 9 21 15 16 27	hdmapcl	|- ( ph -> ( S ` ( F .x. X ) ) e. ( Base ` C ) )
29	1 2 3 9 21 15 16 25	hdmapcl	|- ( ph -> ( S ` X ) e. ( Base ` C ) )
30	21 12 13 14 10 11 22 28 29	lspsneq	|- ( ph -> ( ( L ` { ( S ` ( F .x. X ) ) } ) = ( L ` { ( S ` X ) } ) <-> E. g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
31	20 30	mpbid	|- ( ph -> E. g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )