Theorem hdmap14lem7

Description: Combine cases of F . TODO: Can this be done at once in hdmap14lem3 , in order to get rid of hdmap14lem6 ? Perhaps modify lspsneu to become E! k e. K instead of E! k e. ( K \ { .0. } ) ? (Contributed by NM, 1-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem7.h	|- H = ( LHyp ` K )
2		hdmap14lem7.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmap14lem7.v	|- V = ( Base ` U )
4		hdmap14lem7.t	|- .x. = ( .s ` U )
5		hdmap14lem7.o	|- .0. = ( 0g ` U )
6		hdmap14lem7.r	|- R = ( Scalar ` U )
7		hdmap14lem7.b	|- B = ( Base ` R )
8		hdmap14lem7.c	|- C = ( ( LCDual ` K ) ` W )
9		hdmap14lem7.e	|- .xb = ( .s ` C )
10		hdmap14lem7.p	|- P = ( Scalar ` C )
11		hdmap14lem7.a	|- A = ( Base ` P )
12		hdmap14lem7.s	|- S = ( ( HDMap ` K ) ` W )
13		hdmap14lem7.k	|- ( ph -> ( K e. HL /\ W e. H ) )
14		hdmap14lem7.x	|- ( ph -> X e. ( V \ { .0. } ) )
15		hdmap14lem7.f	|- ( ph -> F e. B )
16		eqid	|- ( 0g ` R ) = ( 0g ` R )
17		eqid	|- ( LSpan ` C ) = ( LSpan ` C )
18		eqid	|- ( 0g ` P ) = ( 0g ` P )
19	13	adantr	|- ( ( ph /\ F = ( 0g ` R ) ) -> ( K e. HL /\ W e. H ) )
20	14	adantr	|- ( ( ph /\ F = ( 0g ` R ) ) -> X e. ( V \ { .0. } ) )
21		simpr	|- ( ( ph /\ F = ( 0g ` R ) ) -> F = ( 0g ` R ) )
22	1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 19 20 21	hdmap14lem6	|- ( ( ph /\ F = ( 0g ` R ) ) -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
23	13	adantr	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> ( K e. HL /\ W e. H ) )
24	14	adantr	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> X e. ( V \ { .0. } ) )
25	15	adantr	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> F e. B )
26		simpr	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> F =/= ( 0g ` R ) )
27		eldifsn	|- ( F e. ( B \ { ( 0g ` R ) } ) <-> ( F e. B /\ F =/= ( 0g ` R ) ) )
28	25 26 27	sylanbrc	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> F e. ( B \ { ( 0g ` R ) } ) )
29	1 2 3 4 5 6 7 16 8 9 17 10 11 18 12 23 24 28	hdmap14lem4	|- ( ( ph /\ F =/= ( 0g ` R ) ) -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
30	22 29	pm2.61dane	|- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )