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 ⊢φ→K∈HL∧W∈H
mapdat.q ⊢φ→Q∈A
Assertion mapdat ⊢φ→M⁡Q∈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 ⊢φ→K∈HL∧W∈H
8 mapdat.q ⊢φ→Q∈A
9 eqid ⊢0U=0U
10 eqid ⊢0C=0C
11 1 2 3 9 5 10 7 mapd0 ⊢φ→M⁡0U=0C
12 eqid ⊢⋖L⁡U=⋖L⁡U
13 1 3 7 dvhlvec ⊢φ→U∈LVec
14 9 4 12 13 8 lsatcv0 ⊢φ→0U⋖L⁡UQ
15 eqid ⊢LSubSp⁡U=LSubSp⁡U
16 eqid ⊢⋖L⁡C=⋖L⁡C
17 1 3 7 dvhlmod ⊢φ→U∈LMod
18 9 15 lsssn0 ⊢U∈LMod→0U∈LSubSp⁡U
19 17 18 syl ⊢φ→0U∈LSubSp⁡U
20 15 4 17 8 lsatlssel ⊢φ→Q∈LSubSp⁡U
21 1 2 3 15 12 5 16 7 19 20 mapdcv ⊢φ→0U⋖L⁡UQ↔M⁡0U⋖L⁡CM⁡Q
22 14 21 mpbid ⊢φ→M⁡0U⋖L⁡CM⁡Q
23 11 22 eqbrtrrd ⊢φ→0C⋖L⁡CM⁡Q
24 eqid ⊢LSubSp⁡C=LSubSp⁡C
25 1 5 7 lcdlvec ⊢φ→C∈LVec
26 1 2 3 15 5 24 7 20 mapdcl2 ⊢φ→M⁡Q∈LSubSp⁡C
27 10 24 6 16 25 26 lsat0cv ⊢φ→M⁡Q∈B↔0C⋖L⁡CM⁡Q
28 23 27 mpbird ⊢φ→M⁡Q∈B