# 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}=\mathrm{LHyp}\left({K}\right)$
mapdat.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
mapdat.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdat.b ${⊢}{B}=\mathrm{LSAtoms}\left({C}\right)$
mapdat.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdcnvat.q ${⊢}{\phi }\to {Q}\in {B}$
Assertion mapdcnvatN ${⊢}{\phi }\to {{M}}^{-1}\left({Q}\right)\in {A}$

### Proof

Step Hyp Ref Expression
1 mapdat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdat.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
5 mapdat.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
6 mapdat.b ${⊢}{B}=\mathrm{LSAtoms}\left({C}\right)$
7 mapdat.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 mapdcnvat.q ${⊢}{\phi }\to {Q}\in {B}$
9 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
10 1 3 7 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
11 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
12 11 9 lsssn0 ${⊢}{U}\in \mathrm{LMod}\to \left\{{0}_{{U}}\right\}\in \mathrm{LSubSp}\left({U}\right)$
13 10 12 syl ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}\in \mathrm{LSubSp}\left({U}\right)$
14 1 2 3 9 7 13 mapdcnvid1N ${⊢}{\phi }\to {{M}}^{-1}\left({M}\left(\left\{{0}_{{U}}\right\}\right)\right)=\left\{{0}_{{U}}\right\}$
15 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
16 1 2 3 11 5 15 7 mapd0 ${⊢}{\phi }\to {M}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{C}}\right\}$
17 16 fveq2d ${⊢}{\phi }\to {{M}}^{-1}\left({M}\left(\left\{{0}_{{U}}\right\}\right)\right)={{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)$
18 14 17 eqtr3d ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}={{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)$
19 eqid ${⊢}{⋖}_{L}\left({C}\right)={⋖}_{L}\left({C}\right)$
20 1 5 7 lcdlvec ${⊢}{\phi }\to {C}\in \mathrm{LVec}$
21 15 6 19 20 8 lsatcv0 ${⊢}{\phi }\to \left\{{0}_{{C}}\right\}{⋖}_{L}\left({C}\right){Q}$
22 1 5 7 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
23 eqid ${⊢}\mathrm{LSubSp}\left({C}\right)=\mathrm{LSubSp}\left({C}\right)$
24 15 23 lsssn0 ${⊢}{C}\in \mathrm{LMod}\to \left\{{0}_{{C}}\right\}\in \mathrm{LSubSp}\left({C}\right)$
25 22 24 syl ${⊢}{\phi }\to \left\{{0}_{{C}}\right\}\in \mathrm{LSubSp}\left({C}\right)$
26 1 2 5 23 7 mapdrn2 ${⊢}{\phi }\to \mathrm{ran}{M}=\mathrm{LSubSp}\left({C}\right)$
27 25 26 eleqtrrd ${⊢}{\phi }\to \left\{{0}_{{C}}\right\}\in \mathrm{ran}{M}$
28 1 2 7 27 mapdcnvid2 ${⊢}{\phi }\to {M}\left({{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)\right)=\left\{{0}_{{C}}\right\}$
29 23 6 22 8 lsatlssel ${⊢}{\phi }\to {Q}\in \mathrm{LSubSp}\left({C}\right)$
30 29 26 eleqtrrd ${⊢}{\phi }\to {Q}\in \mathrm{ran}{M}$
31 1 2 7 30 mapdcnvid2 ${⊢}{\phi }\to {M}\left({{M}}^{-1}\left({Q}\right)\right)={Q}$
32 21 28 31 3brtr4d ${⊢}{\phi }\to {M}\left({{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)\right){⋖}_{L}\left({C}\right){M}\left({{M}}^{-1}\left({Q}\right)\right)$
33 eqid ${⊢}{⋖}_{L}\left({U}\right)={⋖}_{L}\left({U}\right)$
34 1 2 3 9 7 27 mapdcnvcl ${⊢}{\phi }\to {{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
35 1 2 3 9 7 30 mapdcnvcl ${⊢}{\phi }\to {{M}}^{-1}\left({Q}\right)\in \mathrm{LSubSp}\left({U}\right)$
36 1 2 3 9 33 5 19 7 34 35 mapdcv ${⊢}{\phi }\to \left({{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right){⋖}_{L}\left({U}\right){{M}}^{-1}\left({Q}\right)↔{M}\left({{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right)\right){⋖}_{L}\left({C}\right){M}\left({{M}}^{-1}\left({Q}\right)\right)\right)$
37 32 36 mpbird ${⊢}{\phi }\to {{M}}^{-1}\left(\left\{{0}_{{C}}\right\}\right){⋖}_{L}\left({U}\right){{M}}^{-1}\left({Q}\right)$
38 18 37 eqbrtrd ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}{⋖}_{L}\left({U}\right){{M}}^{-1}\left({Q}\right)$
39 1 3 7 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
40 11 9 4 33 39 35 lsat0cv ${⊢}{\phi }\to \left({{M}}^{-1}\left({Q}\right)\in {A}↔\left\{{0}_{{U}}\right\}{⋖}_{L}\left({U}\right){{M}}^{-1}\left({Q}\right)\right)$
41 38 40 mpbird ${⊢}{\phi }\to {{M}}^{-1}\left({Q}\right)\in {A}$