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
|
lspsnel5a |
|- ( 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
|
lspsnel5a |
|- ( 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 ) } ) ) |