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 ⊢ 0 U = 0 U
10 eqid ⊢ 0 C = 0 C
11 1 2 3 9 5 10 7 mapd0 ⊢ φ → M ⁡ 0 U = 0 C
12 eqid ⊢ ⋖ L ⁡ U = ⋖ L ⁡ U
13 1 3 7 dvhlvec ⊢ φ → U ∈ LVec
14 9 4 12 13 8 lsatcv0 ⊢ φ → 0 U ⋖ L ⁡ U Q
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 → 0 U ∈ LSubSp ⁡ U
19 17 18 syl ⊢ φ → 0 U ∈ LSubSp ⁡ U
20 15 4 17 8 lsatlssel ⊢ φ → Q ∈ LSubSp ⁡ U
21 1 2 3 15 12 5 16 7 19 20 mapdcv ⊢ φ → 0 U ⋖ L ⁡ U Q ↔ M ⁡ 0 U ⋖ L ⁡ C M ⁡ Q
22 14 21 mpbid ⊢ φ → M ⁡ 0 U ⋖ L ⁡ C M ⁡ Q
23 11 22 eqbrtrrd ⊢ φ → 0 C ⋖ L ⁡ C M ⁡ 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 ↔ 0 C ⋖ L ⁡ C M ⁡ Q
28 23 27 mpbird ⊢ φ → M ⁡ Q ∈ B