Metamath Proof Explorer

Theorem mapdspex

Description: The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses mapdspex.h 
|- H = ( LHyp ` K )
mapdspex.m 
|- M = ( ( mapd ` K ) ` W )
mapdspex.u 
|- U = ( ( DVecH ` K ) ` W )
mapdspex.v 
|- V = ( Base ` U )
mapdspex.n 
|- N = ( LSpan ` U )
mapdspex.c 
|- C = ( ( LCDual ` K ) ` W )
mapdspex.b 
|- B = ( Base ` C )
mapdspex.j 
|- J = ( LSpan ` C )
mapdspex.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdspex.x 
|- ( ph -> X e. V )
Assertion mapdspex 
|- ( ph -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )

Proof

Step Hyp Ref Expression
1 mapdspex.h 
 |-  H = ( LHyp ` K )
2 mapdspex.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdspex.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapdspex.v 
 |-  V = ( Base ` U )
5 mapdspex.n 
 |-  N = ( LSpan ` U )
6 mapdspex.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 mapdspex.b 
 |-  B = ( Base ` C )
8 mapdspex.j 
 |-  J = ( LSpan ` C )
9 mapdspex.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 mapdspex.x 
 |-  ( ph -> X e. V )
11 1 6 9 lcdlmod 
 |-  ( ph -> C e. LMod )
12 11 adantr 
 |-  ( ( ph /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> C e. LMod )
13 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
14 eqid 
 |-  ( LSAtoms ` C ) = ( LSAtoms ` C )
15 9 adantr 
 |-  ( ( ph /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> ( K e. HL /\ W e. H ) )
16 simpr 
 |-  ( ( ph /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> ( N ` { X } ) e. ( LSAtoms ` U ) )
17 1 2 3 13 6 14 15 16 mapdat 
 |-  ( ( ph /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> ( M ` ( N ` { X } ) ) e. ( LSAtoms ` C ) )
18 7 8 14 islsati 
 |-  ( ( C e. LMod /\ ( M ` ( N ` { X } ) ) e. ( LSAtoms ` C ) ) -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )
19 12 17 18 syl2anc 
 |-  ( ( ph /\ ( N ` { X } ) e. ( LSAtoms ` U ) ) -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )
20 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
21 1 6 7 20 9 lcd0vcl 
 |-  ( ph -> ( 0g ` C ) e. B )
22 21 adantr 
 |-  ( ( ph /\ ( N ` { X } ) = { ( 0g ` U ) } ) -> ( 0g ` C ) e. B )
23 fveq2 
 |-  ( ( N ` { X } ) = { ( 0g ` U ) } -> ( M ` ( N ` { X } ) ) = ( M ` { ( 0g ` U ) } ) )
24 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
25 1 2 3 24 6 20 9 mapd0 
 |-  ( ph -> ( M ` { ( 0g ` U ) } ) = { ( 0g ` C ) } )
26 20 8 lspsn0 
 |-  ( C e. LMod -> ( J ` { ( 0g ` C ) } ) = { ( 0g ` C ) } )
27 11 26 syl 
 |-  ( ph -> ( J ` { ( 0g ` C ) } ) = { ( 0g ` C ) } )
28 25 27 eqtr4d 
 |-  ( ph -> ( M ` { ( 0g ` U ) } ) = ( J ` { ( 0g ` C ) } ) )
29 23 28 sylan9eqr 
 |-  ( ( ph /\ ( N ` { X } ) = { ( 0g ` U ) } ) -> ( M ` ( N ` { X } ) ) = ( J ` { ( 0g ` C ) } ) )
30 sneq 
 |-  ( g = ( 0g ` C ) -> { g } = { ( 0g ` C ) } )
31 30 fveq2d 
 |-  ( g = ( 0g ` C ) -> ( J ` { g } ) = ( J ` { ( 0g ` C ) } ) )
32 31 rspceeqv 
 |-  ( ( ( 0g ` C ) e. B /\ ( M ` ( N ` { X } ) ) = ( J ` { ( 0g ` C ) } ) ) -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )
33 22 29 32 syl2anc 
 |-  ( ( ph /\ ( N ` { X } ) = { ( 0g ` U ) } ) -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )
34 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
35 4 5 24 13 34 10 lsator0sp 
 |-  ( ph -> ( ( N ` { X } ) e. ( LSAtoms ` U ) \/ ( N ` { X } ) = { ( 0g ` U ) } ) )
36 19 33 35 mpjaodan 
 |-  ( ph -> E. g e. B ( M ` ( N ` { X } ) ) = ( J ` { g } ) )