Metamath Proof Explorer

Theorem mapdcnvatN

Description: Atoms are preserved by the map defined by df-mapd . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

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 ) )
mapdcnvat.q 
|- ( ph -> Q e. B )
Assertion mapdcnvatN 
|- ( ph -> ( `' M ` Q ) e. A )

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 mapdcnvat.q 
 |-  ( ph -> Q e. B )
9 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
10 1 3 7 dvhlmod 
 |-  ( ph -> U e. LMod )
11 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
12 11 9 lsssn0 
 |-  ( U e. LMod -> { ( 0g ` U ) } e. ( LSubSp ` U ) )
13 10 12 syl 
 |-  ( ph -> { ( 0g ` U ) } e. ( LSubSp ` U ) )
14 1 2 3 9 7 13 mapdcnvid1N 
 |-  ( ph -> ( `' M ` ( M ` { ( 0g ` U ) } ) ) = { ( 0g ` U ) } )
15 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
16 1 2 3 11 5 15 7 mapd0 
 |-  ( ph -> ( M ` { ( 0g ` U ) } ) = { ( 0g ` C ) } )
17 16 fveq2d 
 |-  ( ph -> ( `' M ` ( M ` { ( 0g ` U ) } ) ) = ( `' M ` { ( 0g ` C ) } ) )
18 14 17 eqtr3d 
 |-  ( ph -> { ( 0g ` U ) } = ( `' M ` { ( 0g ` C ) } ) )
19 eqid 
 |-  (
    20 1 5 7 lcdlvec 
     |-  ( ph -> C e. LVec )
    21 15 6 19 20 8 lsatcv0 
     |-  ( ph -> { ( 0g ` C ) } (
      22 1 5 7 lcdlmod 
       |-  ( ph -> C e. LMod )
      23 eqid 
       |-  ( LSubSp ` C ) = ( LSubSp ` C )
      24 15 23 lsssn0 
       |-  ( C e. LMod -> { ( 0g ` C ) } e. ( LSubSp ` C ) )
      25 22 24 syl 
       |-  ( ph -> { ( 0g ` C ) } e. ( LSubSp ` C ) )
      26 1 2 5 23 7 mapdrn2 
       |-  ( ph -> ran M = ( LSubSp ` C ) )
      27 25 26 eleqtrrd 
       |-  ( ph -> { ( 0g ` C ) } e. ran M )
      28 1 2 7 27 mapdcnvid2 
       |-  ( ph -> ( M ` ( `' M ` { ( 0g ` C ) } ) ) = { ( 0g ` C ) } )
      29 23 6 22 8 lsatlssel 
       |-  ( ph -> Q e. ( LSubSp ` C ) )
      30 29 26 eleqtrrd 
       |-  ( ph -> Q e. ran M )
      31 1 2 7 30 mapdcnvid2 
       |-  ( ph -> ( M ` ( `' M ` Q ) ) = Q )
      32 21 28 31 3brtr4d 
       |-  ( ph -> ( M ` ( `' M ` { ( 0g ` C ) } ) ) (
        33 eqid 
         |-  (
          34 1 2 3 9 7 27 mapdcnvcl 
           |-  ( ph -> ( `' M ` { ( 0g ` C ) } ) e. ( LSubSp ` U ) )
          35 1 2 3 9 7 30 mapdcnvcl 
           |-  ( ph -> ( `' M ` Q ) e. ( LSubSp ` U ) )
          36 1 2 3 9 33 5 19 7 34 35 mapdcv 
           |-  ( ph -> ( ( `' M ` { ( 0g ` C ) } ) ( 
             ( M ` ( `' M ` { ( 0g ` C ) } ) ) (
            37 32 36 mpbird 
             |-  ( ph -> ( `' M ` { ( 0g ` C ) } ) (
              38 18 37 eqbrtrd 
               |-  ( ph -> { ( 0g ` U ) } (
                39 1 3 7 dvhlvec 
                 |-  ( ph -> U e. LVec )
                40 11 9 4 33 39 35 lsat0cv 
                 |-  ( ph -> ( ( `' M ` Q ) e. A <-> { ( 0g ` U ) } (
                  41 38 40 mpbird 
                   |-  ( ph -> ( `' M ` Q ) e. A )