# 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 )`