Metamath Proof Explorer

Theorem hdmapval3lemN

Description: Value of map from vectors to functionals at arguments not colinear with the reference vector E . (Contributed by NM, 17-May-2015) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hdmapval3.h 
 |-  H = ( LHyp ` K )
2 hdmapval3.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapval3.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 hdmapval3.v 
 |-  V = ( Base ` U )
5 hdmapval3.n 
 |-  N = ( LSpan ` U )
6 hdmapval3.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 hdmapval3.d 
 |-  D = ( Base ` C )
8 hdmapval3.j 
 |-  J = ( ( HVMap ` K ) ` W )
9 hdmapval3.i 
 |-  I = ( ( HDMap1 ` K ) ` W )
10 hdmapval3.s 
 |-  S = ( ( HDMap ` K ) ` W )
11 hdmapval3.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmapval3.te 
 |-  ( ph -> ( N ` { T } ) =/= ( N ` { E } ) )
13 hdmapval3lem.t 
 |-  ( ph -> T e. ( V \ { ( 0g ` U ) } ) )
14 hdmapval3lem.x 
 |-  ( ph -> x e. V )
15 hdmapval3lem.xn 
 |-  ( ph -> -. x e. ( N ` { E , T } ) )
16 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
17 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
18 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
19 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
22 1 20 21 3 4 16 2 11 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
23 1 3 4 16 6 7 19 8 11 22 hvmapcl2 
 |-  ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
24 23 eldifad 
 |-  ( ph -> ( J ` E ) e. D )
25 1 3 4 16 5 6 17 18 8 11 22 mapdhvmap 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( N ` { E } ) ) = ( ( LSpan ` C ) ` { ( J ` E ) } ) )
26 1 3 11 dvhlvec 
 |-  ( ph -> U e. LVec )
27 22 eldifad 
 |-  ( ph -> E e. V )
28 13 eldifad 
 |-  ( ph -> T e. V )
29 4 5 26 14 27 28 15 lspindpi 
 |-  ( ph -> ( ( N ` { x } ) =/= ( N ` { E } ) /\ ( N ` { x } ) =/= ( N ` { T } ) ) )
30 29 simpld 
 |-  ( ph -> ( N ` { x } ) =/= ( N ` { E } ) )
31 30 necomd 
 |-  ( ph -> ( N ` { E } ) =/= ( N ` { x } ) )
32 1 3 4 16 5 6 7 17 18 9 11 24 25 31 22 14 hdmap1cl 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , x >. ) e. D )
33 eqidd 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , x >. ) = ( I ` <. E , ( J ` E ) , x >. ) )
34 eqid 
 |-  ( -g ` U ) = ( -g ` U )
35 eqid 
 |-  ( -g ` C ) = ( -g ` C )
36 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
37 1 3 11 dvhlmod 
 |-  ( ph -> U e. LMod )
38 4 36 5 37 27 28 lspprcl 
 |-  ( ph -> ( N ` { E , T } ) e. ( LSubSp ` U ) )
39 16 36 37 38 14 15 lssneln0 
 |-  ( ph -> x e. ( V \ { ( 0g ` U ) } ) )
40 1 3 4 34 16 5 6 7 35 17 18 9 11 22 24 39 32 31 25 hdmap1eq 
 |-  ( ph -> ( ( I ` <. E , ( J ` E ) , x >. ) = ( I ` <. E , ( J ` E ) , x >. ) <-> ( ( ( ( mapd ` K ) ` W ) ` ( N ` { x } ) ) = ( ( LSpan ` C ) ` { ( I ` <. E , ( J ` E ) , x >. ) } ) /\ ( ( ( mapd ` K ) ` W ) ` ( N ` { ( E ( -g ` U ) x ) } ) ) = ( ( LSpan ` C ) ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , x >. ) ) } ) ) ) )
41 33 40 mpbid 
 |-  ( ph -> ( ( ( ( mapd ` K ) ` W ) ` ( N ` { x } ) ) = ( ( LSpan ` C ) ` { ( I ` <. E , ( J ` E ) , x >. ) } ) /\ ( ( ( mapd ` K ) ` W ) ` ( N ` { ( E ( -g ` U ) x ) } ) ) = ( ( LSpan ` C ) ` { ( ( J ` E ) ( -g ` C ) ( I ` <. E , ( J ` E ) , x >. ) ) } ) ) )
42 41 simpld 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( N ` { x } ) ) = ( ( LSpan ` C ) ` { ( I ` <. E , ( J ` E ) , x >. ) } ) )
43 12 necomd 
 |-  ( ph -> ( N ` { E } ) =/= ( N ` { T } ) )
44 4 5 37 27 28 lspprid1 
 |-  ( ph -> E e. ( N ` { E , T } ) )
45 36 5 37 38 44 ellspsn5 
 |-  ( ph -> ( N ` { E } ) C_ ( N ` { E , T } ) )
46 45 45 unssd 
 |-  ( ph -> ( ( N ` { E } ) u. ( N ` { E } ) ) C_ ( N ` { E , T } ) )
47 46 15 ssneldd 
 |-  ( ph -> -. x e. ( ( N ` { E } ) u. ( N ` { E } ) ) )
48 1 2 3 4 5 6 7 8 9 10 11 27 14 47 hdmapval2 
 |-  ( ph -> ( S ` E ) = ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , E >. ) )
49 1 2 8 10 11 hdmapevec 
 |-  ( ph -> ( S ` E ) = ( J ` E ) )
50 48 49 eqtr3d 
 |-  ( ph -> ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , E >. ) = ( J ` E ) )
51 4 5 37 27 28 lspprid2 
 |-  ( ph -> T e. ( N ` { E , T } ) )
52 36 5 37 38 51 ellspsn5 
 |-  ( ph -> ( N ` { T } ) C_ ( N ` { E , T } ) )
53 45 52 unssd 
 |-  ( ph -> ( ( N ` { E } ) u. ( N ` { T } ) ) C_ ( N ` { E , T } ) )
54 53 15 ssneldd 
 |-  ( ph -> -. x e. ( ( N ` { E } ) u. ( N ` { T } ) ) )
55 1 2 3 4 5 6 7 8 9 10 11 28 14 54 hdmapval2 
 |-  ( ph -> ( S ` T ) = ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , T >. ) )
56 55 eqcomd 
 |-  ( ph -> ( I ` <. x , ( I ` <. E , ( J ` E ) , x >. ) , T >. ) = ( S ` T ) )
57 1 3 4 16 5 6 7 17 18 9 11 32 42 39 22 13 43 15 50 56 hdmap1eq4N 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , T >. ) = ( S ` T ) )
58 57 eqcomd 
 |-  ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )