# Metamath Proof Explorer

## Theorem mapdpglem30a

Description: Lemma for mapdpg . (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses mapdpg.h $⊢ H = LHyp ⁡ K$
mapdpg.m $⊢ M = mapd ⁡ K ⁡ W$
mapdpg.u $⊢ U = DVecH ⁡ K ⁡ W$
mapdpg.v $⊢ V = Base U$
mapdpg.s
mapdpg.z
mapdpg.n $⊢ N = LSpan ⁡ U$
mapdpg.c $⊢ C = LCDual ⁡ K ⁡ W$
mapdpg.f $⊢ F = Base C$
mapdpg.r $⊢ R = - C$
mapdpg.j $⊢ J = LSpan ⁡ C$
mapdpg.k $⊢ φ → K ∈ HL ∧ W ∈ H$
mapdpg.x
mapdpg.y
mapdpg.g $⊢ φ → G ∈ F$
mapdpg.ne $⊢ φ → N ⁡ X ≠ N ⁡ Y$
mapdpg.e $⊢ φ → M ⁡ N ⁡ X = J ⁡ G$
Assertion mapdpglem30a $⊢ φ → G ≠ 0 C$

### Proof

Step Hyp Ref Expression
1 mapdpg.h $⊢ H = LHyp ⁡ K$
2 mapdpg.m $⊢ M = mapd ⁡ K ⁡ W$
3 mapdpg.u $⊢ U = DVecH ⁡ K ⁡ W$
4 mapdpg.v $⊢ V = Base U$
5 mapdpg.s
6 mapdpg.z
7 mapdpg.n $⊢ N = LSpan ⁡ U$
8 mapdpg.c $⊢ C = LCDual ⁡ K ⁡ W$
9 mapdpg.f $⊢ F = Base C$
10 mapdpg.r $⊢ R = - C$
11 mapdpg.j $⊢ J = LSpan ⁡ C$
12 mapdpg.k $⊢ φ → K ∈ HL ∧ W ∈ H$
13 mapdpg.x
14 mapdpg.y
15 mapdpg.g $⊢ φ → G ∈ F$
16 mapdpg.ne $⊢ φ → N ⁡ X ≠ N ⁡ Y$
17 mapdpg.e $⊢ φ → M ⁡ N ⁡ X = J ⁡ G$
18 eqid $⊢ LSAtoms ⁡ U = LSAtoms ⁡ U$
19 eqid $⊢ LSAtoms ⁡ C = LSAtoms ⁡ C$
20 1 3 12 dvhlmod $⊢ φ → U ∈ LMod$
21 4 7 6 18 20 13 lsatlspsn $⊢ φ → N ⁡ X ∈ LSAtoms ⁡ U$
22 1 2 3 18 8 19 12 21 mapdat $⊢ φ → M ⁡ N ⁡ X ∈ LSAtoms ⁡ C$
23 17 22 eqeltrrd $⊢ φ → J ⁡ G ∈ LSAtoms ⁡ C$
24 eqid $⊢ 0 C = 0 C$
25 1 8 12 lcdlmod $⊢ φ → C ∈ LMod$
26 9 11 24 19 25 15 lsatspn0 $⊢ φ → J ⁡ G ∈ LSAtoms ⁡ C ↔ G ≠ 0 C$
27 23 26 mpbid $⊢ φ → G ≠ 0 C$