Metamath Proof Explorer

Theorem hdmapval3N

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 } ) )
hdmapval3.t 
|- ( ph -> T e. V )
Assertion hdmapval3N 
|- ( 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 hdmapval3.t 
 |-  ( ph -> T e. V )
14 fveq2 
 |-  ( T = ( 0g ` U ) -> ( S ` T ) = ( S ` ( 0g ` U ) ) )
15 oteq3 
 |-  ( T = ( 0g ` U ) -> <. E , ( J ` E ) , T >. = <. E , ( J ` E ) , ( 0g ` U ) >. )
16 15 fveq2d 
 |-  ( T = ( 0g ` U ) -> ( I ` <. E , ( J ` E ) , T >. ) = ( I ` <. E , ( J ` E ) , ( 0g ` U ) >. ) )
17 14 16 eqeq12d 
 |-  ( T = ( 0g ` U ) -> ( ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) <-> ( S ` ( 0g ` U ) ) = ( I ` <. E , ( J ` E ) , ( 0g ` U ) >. ) ) )
18 eqid 
 |-  ( Base ` K ) = ( Base ` K )
19 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
20 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
21 1 18 19 3 4 20 2 11 dvheveccl 
 |-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
22 21 eldifad 
 |-  ( ph -> E e. V )
23 1 3 4 5 11 22 13 dvh3dim 
 |-  ( ph -> E. x e. V -. x e. ( N ` { E , T } ) )
24 23 adantr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> E. x e. V -. x e. ( N ` { E , T } ) )
25 simp1l 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ph )
26 25 11 syl 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( K e. HL /\ W e. H ) )
27 25 12 syl 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( N ` { T } ) =/= ( N ` { E } ) )
28 25 13 syl 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> T e. V )
29 simp1r 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> T =/= ( 0g ` U ) )
30 eldifsn 
 |-  ( T e. ( V \ { ( 0g ` U ) } ) <-> ( T e. V /\ T =/= ( 0g ` U ) ) )
31 28 29 30 sylanbrc 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> T e. ( V \ { ( 0g ` U ) } ) )
32 simp2 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> x e. V )
33 simp3 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> -. x e. ( N ` { E , T } ) )
34 1 2 3 4 5 6 7 8 9 10 26 27 31 32 33 hdmapval3lemN 
 |-  ( ( ( ph /\ T =/= ( 0g ` U ) ) /\ x e. V /\ -. x e. ( N ` { E , T } ) ) -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
35 34 rexlimdv3a 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( E. x e. V -. x e. ( N ` { E , T } ) -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) ) )
36 24 35 mpd 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
37 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
38 1 3 20 6 37 10 11 hdmapval0 
 |-  ( ph -> ( S ` ( 0g ` U ) ) = ( 0g ` C ) )
39 1 3 4 20 6 7 37 8 11 21 hvmapcl2 
 |-  ( ph -> ( J ` E ) e. ( D \ { ( 0g ` C ) } ) )
40 39 eldifad 
 |-  ( ph -> ( J ` E ) e. D )
41 1 3 4 20 6 7 37 9 11 40 22 hdmap1val0 
 |-  ( ph -> ( I ` <. E , ( J ` E ) , ( 0g ` U ) >. ) = ( 0g ` C ) )
42 38 41 eqtr4d 
 |-  ( ph -> ( S ` ( 0g ` U ) ) = ( I ` <. E , ( J ` E ) , ( 0g ` U ) >. ) )
43 17 36 42 pm2.61ne 
 |-  ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )