hdmapeveclem

Description: Lemma for hdmapevec . TODO: combine with hdmapevec if it shortens overall. (Contributed by NM, 16-May-2015)

	Ref	Expression
Hypotheses	hdmapevec.h	\|- H = ( LHyp ` K )
	hdmapevec.e	\|- E = <. ( _I \|` ( Base ` K ) ) , ( _I \|` ( ( LTrn ` K ) ` W ) ) >.
	hdmapevec.j	\|- J = ( ( HVMap ` K ) ` W )
	hdmapevec.s	\|- S = ( ( HDMap ` K ) ` W )
	hdmapevec.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapevec.u	\|- U = ( ( DVecH ` K ) ` W )
	hdmapevec.v	\|- V = ( Base ` U )
	hdmapevec.n	\|- N = ( LSpan ` U )
	hdmapevec.c	\|- C = ( ( LCDual ` K ) ` W )
	hdmapevec.d	\|- D = ( Base ` C )
	hdmapevec.i	\|- I = ( ( HDMap1 ` K ) ` W )
	hdmapevec.x	\|- ( ph -> X e. V )
	hdmapevec.ne	\|- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { E } ) ) )
Assertion	hdmapeveclem	\|- ( ph -> ( S ` E ) = ( J ` E ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapevec.h	\|- H = ( LHyp ` K )
2		hdmapevec.e	\|- E = <. ( _I \|` ( Base ` K ) ) , ( _I \|` ( ( LTrn ` K ) ` W ) ) >.
3		hdmapevec.j	\|- J = ( ( HVMap ` K ) ` W )
4		hdmapevec.s	\|- S = ( ( HDMap ` K ) ` W )
5		hdmapevec.k	\|- ( ph -> ( K e. HL /\ W e. H ) )
6		hdmapevec.u	\|- U = ( ( DVecH ` K ) ` W )
7		hdmapevec.v	\|- V = ( Base ` U )
8		hdmapevec.n	\|- N = ( LSpan ` U )
9		hdmapevec.c	\|- C = ( ( LCDual ` K ) ` W )
10		hdmapevec.d	\|- D = ( Base ` C )
11		hdmapevec.i	\|- I = ( ( HDMap1 ` K ) ` W )
12		hdmapevec.x	\|- ( ph -> X e. V )
13		hdmapevec.ne	\|- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { E } ) ) )
14		eqid	\|- ( Base ` K ) = ( Base ` K )
15		eqid	\|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
16		eqid	\|- ( 0g ` U ) = ( 0g ` U )
17	1 14 15 6 7 16 2 5	dvheveccl	\|- ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
18	17	eldifad	\|- ( ph -> E e. V )
19	1 2 6 7 8 9 10 3 11 4 5 18 12 13	hdmapval2	\|- ( ph -> ( S ` E ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , E >. ) )
20		eqid	\|- ( LSpan ` C ) = ( LSpan ` C )
21		eqid	\|- ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
22		eqid	\|- ( 0g ` C ) = ( 0g ` C )
23	1 6 7 16 9 10 22 3 5 17	hvmapcl2	\|- ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
24	23	eldifad	\|- ( ph -> ( J ` E ) e. D )
25	1 6 7 16 8 9 20 21 3 5 17	mapdhvmap	\|- ( ph -> ( ( ( mapd ` K ) ` W ) ` ( N ` { E } ) ) = ( ( LSpan ` C ) ` { ( J ` E ) } ) )
26	1 6 5	dvhlmod	\|- ( ph -> U e. LMod )
27	7 8 26 12 13 18	hdmaplem1	\|- ( ph -> ( N ` { X } ) =/= ( N ` { E } ) )
28	27	necomd	\|- ( ph -> ( N ` { E } ) =/= ( N ` { X } ) )
29	7 8 26 12 13 18 16	hdmaplem3	\|- ( ph -> X e. ( V \ { ( 0g ` U ) } ) )
30		eqidd	\|- ( ph -> ( I ` <. E , ( J ` E ) , X >. ) = ( I ` <. E , ( J ` E ) , X >. ) )
31	1 6 7 16 8 9 10 20 21 11 5 24 25 28 17 29 30	hdmap1eq2	\|- ( ph -> ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , E >. ) = ( J ` E ) )
32	19 31	eqtrd	\|- ( ph -> ( S ` E ) = ( J ` E ) )

Metamath Proof Explorer

Theorem hdmapeveclem

Proof