Metamath Proof Explorer

Theorem mapdpglem2a

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

Ref Expression
Hypotheses mapdpglem.h ⊢ H = LHyp ⁡ K
mapdpglem.m ⊢ M = mapd ⁡ K ⁡ W
mapdpglem.u ⊢ U = DVecH ⁡ K ⁡ W
mapdpglem.v ⊢ V = Base U
mapdpglem.s ⊢ - ˙ = - U
mapdpglem.n ⊢ N = LSpan ⁡ U
mapdpglem.c ⊢ C = LCDual ⁡ K ⁡ W
mapdpglem.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdpglem.x ⊢ φ → X ∈ V
mapdpglem.y ⊢ φ → Y ∈ V
mapdpglem1.p ⊢ ⊕ ˙ = LSSum ⁡ C
mapdpglem2.j ⊢ J = LSpan ⁡ C
mapdpglem3.f ⊢ F = Base C
mapdpglem3.te ⊢ φ → t ∈ M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y
Assertion mapdpglem2a ⊢ φ → t ∈ F

Proof

Step Hyp Ref Expression
1 mapdpglem.h ⊢ H = LHyp ⁡ K
2 mapdpglem.m ⊢ M = mapd ⁡ K ⁡ W
3 mapdpglem.u ⊢ U = DVecH ⁡ K ⁡ W
4 mapdpglem.v ⊢ V = Base U
5 mapdpglem.s ⊢ - ˙ = - U
6 mapdpglem.n ⊢ N = LSpan ⁡ U
7 mapdpglem.c ⊢ C = LCDual ⁡ K ⁡ W
8 mapdpglem.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 mapdpglem.x ⊢ φ → X ∈ V
10 mapdpglem.y ⊢ φ → Y ∈ V
11 mapdpglem1.p ⊢ ⊕ ˙ = LSSum ⁡ C
12 mapdpglem2.j ⊢ J = LSpan ⁡ C
13 mapdpglem3.f ⊢ F = Base C
14 mapdpglem3.te ⊢ φ → t ∈ M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y
15 1 7 8 lcdlmod ⊢ φ → C ∈ LMod
16 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
17 eqid ⊢ LSubSp ⁡ C = LSubSp ⁡ C
18 1 3 8 dvhlmod ⊢ φ → U ∈ LMod
19 4 16 6 lspsncl ⊢ U ∈ LMod ∧ X ∈ V → N ⁡ X ∈ LSubSp ⁡ U
20 18 9 19 syl2anc ⊢ φ → N ⁡ X ∈ LSubSp ⁡ U
21 1 2 3 16 7 17 8 20 mapdcl2 ⊢ φ → M ⁡ N ⁡ X ∈ LSubSp ⁡ C
22 4 16 6 lspsncl ⊢ U ∈ LMod ∧ Y ∈ V → N ⁡ Y ∈ LSubSp ⁡ U
23 18 10 22 syl2anc ⊢ φ → N ⁡ Y ∈ LSubSp ⁡ U
24 1 2 3 16 7 17 8 23 mapdcl2 ⊢ φ → M ⁡ N ⁡ Y ∈ LSubSp ⁡ C
25 17 11 lsmcl ⊢ C ∈ LMod ∧ M ⁡ N ⁡ X ∈ LSubSp ⁡ C ∧ M ⁡ N ⁡ Y ∈ LSubSp ⁡ C → M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y ∈ LSubSp ⁡ C
26 15 21 24 25 syl3anc ⊢ φ → M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y ∈ LSubSp ⁡ C
27 13 17 lssel ⊢ M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y ∈ LSubSp ⁡ C ∧ t ∈ M ⁡ N ⁡ X ⊕ ˙ M ⁡ N ⁡ Y → t ∈ F
28 26 14 27 syl2anc ⊢ φ → t ∈ F