# 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}=\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)$
mapdat.q ${⊢}{\phi }\to {Q}\in {A}$
Assertion mapdat ${⊢}{\phi }\to {M}\left({Q}\right)\in {B}$

### 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 mapdat.q ${⊢}{\phi }\to {Q}\in {A}$
9 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
10 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
11 1 2 3 9 5 10 7 mapd0 ${⊢}{\phi }\to {M}\left(\left\{{0}_{{U}}\right\}\right)=\left\{{0}_{{C}}\right\}$
12 eqid ${⊢}{⋖}_{L}\left({U}\right)={⋖}_{L}\left({U}\right)$
13 1 3 7 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
14 9 4 12 13 8 lsatcv0 ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}{⋖}_{L}\left({U}\right){Q}$
15 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
16 eqid ${⊢}{⋖}_{L}\left({C}\right)={⋖}_{L}\left({C}\right)$
17 1 3 7 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
18 9 15 lsssn0 ${⊢}{U}\in \mathrm{LMod}\to \left\{{0}_{{U}}\right\}\in \mathrm{LSubSp}\left({U}\right)$
19 17 18 syl ${⊢}{\phi }\to \left\{{0}_{{U}}\right\}\in \mathrm{LSubSp}\left({U}\right)$
20 15 4 17 8 lsatlssel ${⊢}{\phi }\to {Q}\in \mathrm{LSubSp}\left({U}\right)$
21 1 2 3 15 12 5 16 7 19 20 mapdcv ${⊢}{\phi }\to \left(\left\{{0}_{{U}}\right\}{⋖}_{L}\left({U}\right){Q}↔{M}\left(\left\{{0}_{{U}}\right\}\right){⋖}_{L}\left({C}\right){M}\left({Q}\right)\right)$
22 14 21 mpbid ${⊢}{\phi }\to {M}\left(\left\{{0}_{{U}}\right\}\right){⋖}_{L}\left({C}\right){M}\left({Q}\right)$
23 11 22 eqbrtrrd ${⊢}{\phi }\to \left\{{0}_{{C}}\right\}{⋖}_{L}\left({C}\right){M}\left({Q}\right)$
24 eqid ${⊢}\mathrm{LSubSp}\left({C}\right)=\mathrm{LSubSp}\left({C}\right)$
25 1 5 7 lcdlvec ${⊢}{\phi }\to {C}\in \mathrm{LVec}$
26 1 2 3 15 5 24 7 20 mapdcl2 ${⊢}{\phi }\to {M}\left({Q}\right)\in \mathrm{LSubSp}\left({C}\right)$
27 10 24 6 16 25 26 lsat0cv ${⊢}{\phi }\to \left({M}\left({Q}\right)\in {B}↔\left\{{0}_{{C}}\right\}{⋖}_{L}\left({C}\right){M}\left({Q}\right)\right)$
28 23 27 mpbird ${⊢}{\phi }\to {M}\left({Q}\right)\in {B}$