Metamath Proof Explorer

Theorem hdmapcl

Description: Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapcl.h 
|- H = ( LHyp ` K )
hdmapcl.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapcl.v 
|- V = ( Base ` U )
hdmapcl.c 
|- C = ( ( LCDual ` K ) ` W )
hdmapcl.d 
|- D = ( Base ` C )
hdmapcl.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapcl.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapcl.t 
|- ( ph -> T e. V )
Assertion hdmapcl 
|- ( ph -> ( S ` T ) e. D )

Proof

Step Hyp Ref Expression
1 hdmapcl.h 
 |-  H = ( LHyp ` K )
2 hdmapcl.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapcl.v 
 |-  V = ( Base ` U )
4 hdmapcl.c 
 |-  C = ( ( LCDual ` K ) ` W )
5 hdmapcl.d 
 |-  D = ( Base ` C )
6 hdmapcl.s 
 |-  S = ( ( HDMap ` K ) ` W )
7 hdmapcl.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 hdmapcl.t 
 |-  ( ph -> T e. V )
9 eqid 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
10 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
11 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
12 eqid 
 |-  ( ( HDMap1 ` K ) ` W ) = ( ( HDMap1 ` K ) ` W )
13 1 9 2 3 10 4 5 11 12 6 7 8 hdmapval 
 |-  ( ph -> ( S ` T ) = ( iota_ h e. D A. y e. V ( -. y e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { T } ) ) -> h = ( ( ( HDMap1 ` K ) ` W ) ` <. y , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , y >. ) , T >. ) ) ) )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
16 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
19 1 17 18 2 3 14 9 7 dvheveccl 
 |-  ( ph -> <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. e. ( V \ { ( 0g ` U ) } ) )
20 1 2 3 14 10 4 15 16 11 7 19 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 ) ) >. ) } ) )
21 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
22 1 2 3 14 4 5 21 11 7 19 hvmapcl2 
 |-  ( ph -> ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) e. ( D \ { ( 0g ` C ) } ) )
23 22 eldifad 
 |-  ( ph -> ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) e. D )
24 1 2 3 14 10 4 5 15 16 12 7 20 19 23 8 hdmap1eu 
 |-  ( ph -> E! h e. D A. y e. V ( -. y e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { T } ) ) -> h = ( ( ( HDMap1 ` K ) ` W ) ` <. y , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , y >. ) , T >. ) ) )
25 riotacl 
 |-  ( E! h e. D A. y e. V ( -. y e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { T } ) ) -> h = ( ( ( HDMap1 ` K ) ` W ) ` <. y , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , y >. ) , T >. ) ) -> ( iota_ h e. D A. y e. V ( -. y e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { T } ) ) -> h = ( ( ( HDMap1 ` K ) ` W ) ` <. y , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , y >. ) , T >. ) ) ) e. D )
26 24 25 syl 
 |-  ( ph -> ( iota_ h e. D A. y e. V ( -. y e. ( ( ( LSpan ` U ) ` { <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. } ) u. ( ( LSpan ` U ) ` { T } ) ) -> h = ( ( ( HDMap1 ` K ) ` W ) ` <. y , ( ( ( HDMap1 ` K ) ` W ) ` <. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. , ( ( ( HVMap ` K ) ` W ) ` <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. ) , y >. ) , T >. ) ) ) e. D )
27 13 26 eqeltrd 
 |-  ( ph -> ( S ` T ) e. D )