Metamath Proof Explorer

Theorem hdmap10lem

Description: Lemma for hdmap10 . (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmap10.h 
|- H = ( LHyp ` K )
hdmap10.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap10.v 
|- V = ( Base ` U )
hdmap10.n 
|- N = ( LSpan ` U )
hdmap10.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap10.l 
|- L = ( LSpan ` C )
hdmap10.m 
|- M = ( ( mapd ` K ) ` W )
hdmap10.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap10.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap10.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmap10.o 
|- .0. = ( 0g ` U )
hdmap10.d 
|- D = ( Base ` C )
hdmap10.j 
|- J = ( ( HVMap ` K ) ` W )
hdmap10.i 
|- I = ( ( HDMap1 ` K ) ` W )
hdmap10lem.t 
|- ( ph -> T e. ( V \ { .0. } ) )
Assertion hdmap10lem 
|- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )

Proof

Step Hyp Ref Expression
1 hdmap10.h 
 |-  H = ( LHyp ` K )
2 hdmap10.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap10.v 
 |-  V = ( Base ` U )
4 hdmap10.n 
 |-  N = ( LSpan ` U )
5 hdmap10.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmap10.l 
 |-  L = ( LSpan ` C )
7 hdmap10.m 
 |-  M = ( ( mapd ` K ) ` W )
8 hdmap10.s 
 |-  S = ( ( HDMap ` K ) ` W )
9 hdmap10.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 hdmap10.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
11 hdmap10.o 
 |-  .0. = ( 0g ` U )
12 hdmap10.d 
 |-  D = ( Base ` C )
13 hdmap10.j 
 |-  J = ( ( HVMap ` K ) ` W )
14 hdmap10.i 
 |-  I = ( ( HDMap1 ` K ) ` W )
15 hdmap10lem.t 
 |-  ( ph -> T e. ( V \ { .0. } ) )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
18 1 16 17 2 3 11 10 9 dvheveccl 
 |-  ( ph -> E e. ( V \ { .0. } ) )
19 18 eldifad 
 |-  ( ph -> E e. V )
20 15 eldifad 
 |-  ( ph -> T e. V )
21 1 2 3 4 9 19 20 dvh3dim 
 |-  ( ph -> E. x e. V -. x e. ( N ` { E , T } ) )
22 9 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( K e. HL /\ W e. H ) )
23 20 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> T e. V )
24 simp2 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> x e. V )
25 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
26 1 2 9 dvhlmod 
 |-  ( ph -> U e. LMod )
27 3 25 4 26 19 20 lspprcl 
 |-  ( ph -> ( N ` { E , T } ) e. ( LSubSp ` U ) )
28 3 4 26 19 20 lspprid1 
 |-  ( ph -> E e. ( N ` { E , T } ) )
29 25 4 26 27 28 ellspsn5 
 |-  ( ph -> ( N ` { E } ) C_ ( N ` { E , T } ) )
30 3 4 26 19 20 lspprid2 
 |-  ( ph -> T e. ( N ` { E , T } ) )
31 25 4 26 27 30 ellspsn5 
 |-  ( ph -> ( N ` { T } ) C_ ( N ` { E , T } ) )
32 29 31 unssd 
 |-  ( ph -> ( ( N ` { E } ) u. ( N ` { T } ) ) C_ ( N ` { E , T } ) )
33 32 sseld 
 |-  ( ph -> ( x e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> x e. ( N ` { E , T } ) ) )
34 33 con3dimp 
 |-  ( ( ph /\ -. x e. ( N ` { E , T } ) ) -> -. x e. ( ( N ` { E } ) u. ( N ` { T } ) ) )
35 34 3adant2 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> -. x e. ( ( N ` { E } ) u. ( N ` { T } ) ) )
36 1 10 2 3 4 5 12 13 14 8 22 23 24 35 hdmapval2 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( S ` T ) = ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , T >. ) )
37 36 eqcomd 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , T >. ) = ( S ` T ) )
38 eqid 
 |-  ( -g ` U ) = ( -g ` U )
39 eqid 
 |-  ( -g ` C ) = ( -g ` C )
40 26 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> U e. LMod )
41 27 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( N ` { E , T } ) e. ( LSubSp ` U ) )
42 simp3 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> -. x e. ( N ` { E , T } ) )
43 11 25 40 41 24 42 lssneln0 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> x e. ( V \ { .0. } ) )
44 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
45 1 2 3 11 5 12 44 13 9 18 hvmapcl2 
 |-  ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
46 45 eldifad 
 |-  ( ph -> ( J ` E ) e. D )
47 46 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( J ` E ) e. D )
48 1 2 3 11 4 5 6 7 13 9 18 mapdhvmap 
 |-  ( ph -> ( M ` ( N ` { E } ) ) = ( L ` { ( J ` E ) } ) )
49 48 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( M ` ( N ` { E } ) ) = ( L ` { ( J ` E ) } ) )
50 1 2 9 dvhlvec 
 |-  ( ph -> U e. LVec )
51 50 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> U e. LVec )
52 19 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> E e. V )
53 3 4 51 24 52 23 42 lspindpi 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( ( N ` { x } ) =/= ( N ` { E } ) /\ ( N ` { x } ) =/= ( N ` { T } ) ) )
54 53 simpld 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( N ` { x } ) =/= ( N ` { E } ) )
55 54 necomd 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( N ` { E } ) =/= ( N ` { x } ) )
56 18 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> E e. ( V \ { .0. } ) )
57 1 2 3 11 4 5 12 6 7 14 22 47 49 55 56 24 hdmap1cl 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( I ` <. E , ( J ` E ) , x >. ) e. D )
58 15 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> T e. ( V \ { .0. } ) )
59 1 2 3 5 12 8 9 20 hdmapcl 
 |-  ( ph -> ( S ` T ) e. D )
60 59 3ad2ant1 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( S ` T ) e. D )
61 53 simprd 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( N ` { x } ) =/= ( N ` { T } ) )
62 eqid 
 |-  ( I ` <. E , ( J ` E ) , x >. ) = ( I ` <. E , ( J ` E ) , x >. )
63 1 2 3 38 11 4 5 12 39 6 7 14 22 56 47 43 57 55 49 hdmap1eq 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( ( I ` <. E , ( J ` E ) , x >. ) = ( I ` <. E , ( J ` E ) , x >. ) <-> ( ( M ` ( N ` { x } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , x >. ) } ) /\ ( M ` ( N ` { ( E ( -g ` U ) x ) } ) ) = ( L ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , x >. ) ) } ) ) ) )
64 62 63 mpbii 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( ( M ` ( N ` { x } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , x >. ) } ) /\ ( M ` ( N ` { ( E ( -g ` U ) x ) } ) ) = ( L ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , x >. ) ) } ) ) )
65 64 simpld 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( M ` ( N ` { x } ) ) = ( L ` { ( I ` <. E , ( J ` E ) , x >. ) } ) )
66 1 2 3 38 11 4 5 12 39 6 7 14 22 43 57 58 60 61 65 hdmap1eq 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , T >. ) = ( S ` T ) <-> ( ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) /\ ( M ` ( N ` { ( x ( -g ` U ) T ) } ) ) = ( L ` { ( ( I ` <. E , ( J ` E ) , x >. ) ( -g ` C ) ( S ` T ) ) } ) ) ) )
67 37 66 mpbid 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) /\ ( M ` ( N ` { ( x ( -g ` U ) T ) } ) ) = ( L ` { ( ( I ` <. E , ( J ` E ) , x >. ) ( -g ` C ) ( S ` T ) ) } ) ) )
68 67 simpld 
 |-  ( ( ph /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
69 68 rexlimdv3a 
 |-  ( ph -> ( E. x e. V -. x e. ( N ` { E , T } ) -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) ) )
70 21 69 mpd 
 |-  ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )