Theorem hdmap14lem4a

Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. (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	hdmap14lem4a	|- ( ph -> ( E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( 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		eqid	|- ( 0g ` C ) = ( 0g ` C )
20		eqid	|- ( Base ` C ) = ( Base ` C )
21	1 2 16	dvhlmod	|- ( ph -> U e. LMod )
22	18	eldifad	|- ( ph -> F e. B )
23	17	eldifad	|- ( ph -> X e. V )
24	3 6 4 7	lmodvscl	|- ( ( U e. LMod /\ F e. B /\ X e. V ) -> ( F .x. X ) e. V )
25	21 22 23 24	syl3anc	|- ( ph -> ( F .x. X ) e. V )
26		eldifsni	|- ( F e. ( B \ { Z } ) -> F =/= Z )
27	18 26	syl	|- ( ph -> F =/= Z )
28		eldifsni	|- ( X e. ( V \ { .0. } ) -> X =/= .0. )
29	17 28	syl	|- ( ph -> X =/= .0. )
30	1 2 16	dvhlvec	|- ( ph -> U e. LVec )
31	3 4 6 7 8 5 30 22 23	lvecvsn0	|- ( ph -> ( ( F .x. X ) =/= .0. <-> ( F =/= Z /\ X =/= .0. ) ) )
32	27 29 31	mpbir2and	|- ( ph -> ( F .x. X ) =/= .0. )
33		eldifsn	|- ( ( F .x. X ) e. ( V \ { .0. } ) <-> ( ( F .x. X ) e. V /\ ( F .x. X ) =/= .0. ) )
34	25 32 33	sylanbrc	|- ( ph -> ( F .x. X ) e. ( V \ { .0. } ) )
35	1 2 3 5 9 19 20 15 16 34	hdmapnzcl	|- ( ph -> ( S ` ( F .x. X ) ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) )
36		eldifsni	|- ( ( S ` ( F .x. X ) ) e. ( ( Base ` C ) \ { ( 0g ` C ) } ) -> ( S ` ( F .x. X ) ) =/= ( 0g ` C ) )
37	35 36	syl	|- ( ph -> ( S ` ( F .x. X ) ) =/= ( 0g ` C ) )
38	37	adantr	|- ( ( ph /\ g e. { Q } ) -> ( S ` ( F .x. X ) ) =/= ( 0g ` C ) )
39		elsni	|- ( g e. { Q } -> g = Q )
40	39	oveq1d	|- ( g e. { Q } -> ( g .xb ( S ` X ) ) = ( Q .xb ( S ` X ) ) )
41	1 9 16	lcdlmod	|- ( ph -> C e. LMod )
42	1 2 3 9 20 15 16 23	hdmapcl	|- ( ph -> ( S ` X ) e. ( Base ` C ) )
43	20 12 10 14 19	lmod0vs	|- ( ( C e. LMod /\ ( S ` X ) e. ( Base ` C ) ) -> ( Q .xb ( S ` X ) ) = ( 0g ` C ) )
44	41 42 43	syl2anc	|- ( ph -> ( Q .xb ( S ` X ) ) = ( 0g ` C ) )
45	40 44	sylan9eqr	|- ( ( ph /\ g e. { Q } ) -> ( g .xb ( S ` X ) ) = ( 0g ` C ) )
46	38 45	neeqtrrd	|- ( ( ph /\ g e. { Q } ) -> ( S ` ( F .x. X ) ) =/= ( g .xb ( S ` X ) ) )
47	46	neneqd	|- ( ( ph /\ g e. { Q } ) -> -. ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
48	47	nrexdv	|- ( ph -> -. E. g e. { Q } ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
49		reuun2	|- ( -. E. g e. { Q } ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) -> ( E! g e. ( ( A \ { Q } ) u. { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
50	48 49	syl	|- ( ph -> ( E! g e. ( ( A \ { Q } ) u. { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
51	12 13 14	lmod0cl	|- ( C e. LMod -> Q e. A )
52		difsnid	|- ( Q e. A -> ( ( A \ { Q } ) u. { Q } ) = A )
53		reueq1	|- ( ( ( A \ { Q } ) u. { Q } ) = A -> ( E! g e. ( ( A \ { Q } ) u. { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
54	41 51 52 53	4syl	|- ( ph -> ( E! g e. ( ( A \ { Q } ) u. { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
55	50 54	bitr3d	|- ( ph -> ( E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )