Metamath Proof Explorer

Theorem hdmapval0

Description: Value of map from vectors to functionals at zero. Note: we use dvh3dim for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmapval0.h 
|- H = ( LHyp ` K )
hdmapval0.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapval0.o 
|- .0. = ( 0g ` U )
hdmapval0.c 
|- C = ( ( LCDual ` K ) ` W )
hdmapval0.q 
|- Q = ( 0g ` C )
hdmapval0.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapval0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hdmapval0 
|- ( ph -> ( S ` .0. ) = Q )

Proof

Step Hyp Ref Expression
1 hdmapval0.h 
 |-  H = ( LHyp ` K )
2 hdmapval0.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapval0.o 
 |-  .0. = ( 0g ` U )
4 hdmapval0.c 
 |-  C = ( ( LCDual ` K ) ` W )
5 hdmapval0.q 
 |-  Q = ( 0g ` C )
6 hdmapval0.s 
 |-  S = ( ( HDMap ` K ) ` W )
7 hdmapval0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 eqid 
 |-  ( Base ` U ) = ( Base ` U )
9 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
12 eqid 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
13 1 10 11 2 8 3 12 7 dvheveccl 
 |-  ( ph -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( ( Base ` U ) \ { .0. } ) )
14 13 eldifad 
 |-  ( ph -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( Base ` U ) )
15 1 2 7 dvhlmod 
 |-  ( ph -> U e. LMod )
16 8 3 lmod0vcl 
 |-  ( U e. LMod -> .0. e. ( Base ` U ) )
17 15 16 syl 
 |-  ( ph -> .0. e. ( Base ` U ) )
18 1 2 8 9 7 14 17 dvh3dim 
 |-  ( ph -> E. x e. ( Base ` U ) -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
19 eqid 
 |-  ( Base ` C ) = ( Base ` C )
20 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
21 eqid 
 |-  ( ( HDMap1 ` K ) ` W ) = ( ( HDMap1 ` K ) ` W )
22 7 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( K e. HL /\ W e. H ) )
23 17 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> .0. e. ( Base ` U ) )
24 simp2 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> x e. ( Base ` U ) )
25 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
26 8 25 9 15 14 17 lspprcl 
 |-  ( ph -> ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) e. ( LSubSp ` U ) )
27 8 9 15 14 17 lspprid1 
 |-  ( ph -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
28 25 9 15 26 27 lspsnel5a 
 |-  ( ph -> ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) C_ ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
29 8 9 15 14 17 lspprid2 
 |-  ( ph -> .0. e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
30 25 9 15 26 29 lspsnel5a 
 |-  ( ph -> ( ( LSpan ` U ) ` { .0. } ) C_ ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
31 28 30 unssd 
 |-  ( ph -> ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { .0. } ) ) C_ ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
32 31 ssneld 
 |-  ( ph -> ( -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) -> -. x e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { .0. } ) ) ) )
33 32 adantr 
 |-  ( ( ph /\ x e. ( Base ` U ) ) -> ( -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) -> -. x e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { .0. } ) ) ) )
34 33 3impia 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> -. x e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { .0. } ) ) )
35 1 12 2 8 9 4 19 20 21 6 22 23 24 34 hdmapval2 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( S ` .0. ) = ( ( ( HDMap1 ` K ) ` W ) ` <. x , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , x >. ) , .0. >. ) )
36 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
37 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
38 1 2 8 3 4 19 5 20 7 13 hvmapcl2 
 |-  ( ph -> ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) e. ( ( Base ` C ) \ { Q } ) )
39 38 eldifad 
 |-  ( ph -> ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) e. ( Base ` C ) )
40 39 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) e. ( Base ` C ) )
41 1 2 8 3 9 4 36 37 20 7 13 mapdhvmap 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) ) = ( ( LSpan ` C ) ` { ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) } ) )
42 41 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) ) = ( ( LSpan ` C ) ` { ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) } ) )
43 1 2 7 dvhlvec 
 |-  ( ph -> U e. LVec )
44 43 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> U e. LVec )
45 14 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( Base ` U ) )
46 simp3 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) )
47 8 9 44 24 45 23 46 lspindpi 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( ( LSpan ` U ) ` { x } ) =/= ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) /\ ( ( LSpan ` U ) ` { x } ) =/= ( ( LSpan ` U ) ` { .0. } ) ) )
48 47 simpld 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( LSpan ` U ) ` { x } ) =/= ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) )
49 48 necomd 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) =/= ( ( LSpan ` U ) ` { x } ) )
50 13 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( ( Base ` U ) \ { .0. } ) )
51 1 2 8 3 9 4 19 36 37 21 22 40 42 49 50 24 hdmap1cl 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , x >. ) e. ( Base ` C ) )
52 1 2 8 3 4 19 5 21 22 51 24 hdmap1val0 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( ( ( HDMap1 ` K ) ` W ) ` <. x , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , x >. ) , .0. >. ) = Q )
53 35 52 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` U ) /\ -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) ) -> ( S ` .0. ) = Q )
54 53 rexlimdv3a 
 |-  ( ph -> ( E. x e. ( Base ` U ) -. x e. ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , .0. } ) -> ( S ` .0. ) = Q ) )
55 18 54 mpd 
 |-  ( ph -> ( S ` .0. ) = Q )