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=BaseU
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=BaseC
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=BaseU
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=BaseC
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