Metamath Proof Explorer

Theorem mapdat

Description: Atoms are preserved by the map defined by df-mapd . Property (g) in Baer p. 41. (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses mapdat.h 
|- H = ( LHyp ` K )
mapdat.m 
|- M = ( ( mapd ` K ) ` W )
mapdat.u 
|- U = ( ( DVecH ` K ) ` W )
mapdat.a 
|- A = ( LSAtoms ` U )
mapdat.c 
|- C = ( ( LCDual ` K ) ` W )
mapdat.b 
|- B = ( LSAtoms ` C )
mapdat.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdat.q 
|- ( ph -> Q e. A )
Assertion mapdat 
|- ( ph -> ( M ` Q ) e. B )

Proof

Step Hyp Ref Expression
1 mapdat.h 
 |-  H = ( LHyp ` K )
2 mapdat.m 
 |-  M = ( ( mapd ` K ) ` W )
3 mapdat.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 mapdat.a 
 |-  A = ( LSAtoms ` U )
5 mapdat.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 mapdat.b 
 |-  B = ( LSAtoms ` C )
7 mapdat.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 mapdat.q 
 |-  ( ph -> Q e. A )
9 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
10 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
11 1 2 3 9 5 10 7 mapd0 
 |-  ( ph -> ( M ` { ( 0g ` U ) } ) = { ( 0g ` C ) } )
12 eqid 
 |-  (
    13 1 3 7 dvhlvec 
     |-  ( ph -> U e. LVec )
    14 9 4 12 13 8 lsatcv0 
     |-  ( ph -> { ( 0g ` U ) } (
      15 eqid 
       |-  ( LSubSp ` U ) = ( LSubSp ` U )
      16 eqid 
       |-  (
        17 1 3 7 dvhlmod 
         |-  ( ph -> U e. LMod )
        18 9 15 lsssn0 
         |-  ( U e. LMod -> { ( 0g ` U ) } e. ( LSubSp ` U ) )
        19 17 18 syl 
         |-  ( ph -> { ( 0g ` U ) } e. ( LSubSp ` U ) )
        20 15 4 17 8 lsatlssel 
         |-  ( ph -> Q e. ( LSubSp ` U ) )
        21 1 2 3 15 12 5 16 7 19 20 mapdcv 
         |-  ( ph -> ( { ( 0g ` U ) } ( 
           ( M ` { ( 0g ` U ) } ) (
          22 14 21 mpbid 
           |-  ( ph -> ( M ` { ( 0g ` U ) } ) (
            23 11 22 eqbrtrrd 
             |-  ( ph -> { ( 0g ` C ) } (
              24 eqid 
               |-  ( LSubSp ` C ) = ( LSubSp ` C )
              25 1 5 7 lcdlvec 
               |-  ( ph -> C e. LVec )
              26 1 2 3 15 5 24 7 20 mapdcl2 
               |-  ( ph -> ( M ` Q ) e. ( LSubSp ` C ) )
              27 10 24 6 16 25 26 lsat0cv 
               |-  ( ph -> ( ( M ` Q ) e. B <-> { ( 0g ` C ) } (
                28 23 27 mpbird 
                 |-  ( ph -> ( M ` Q ) e. B )