Metamath Proof Explorer

Theorem mapdlsmcl

Description: Closure of dual subspace sum for the map defined by df-mapd . (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses mapdlsmcl.h ⊢H=LHyp⁡K
mapdlsmcl.m ⊢M=mapd⁡K⁡W
mapdlsmcl.u ⊢U=DVecH⁡K⁡W
mapdlsmcl.c ⊢C=LCDual⁡K⁡W
mapdlsmcl.p ⊢⊕˙=LSSum⁡C
mapdlsmcl.k ⊢φ→K∈HL∧W∈H
mapdlsmcl.x ⊢φ→X∈ran⁡M
mapdlsmcl.y ⊢φ→Y∈ran⁡M
Assertion mapdlsmcl ⊢φ→X⊕˙Y∈ran⁡M

Proof

Step Hyp Ref Expression
1 mapdlsmcl.h ⊢H=LHyp⁡K
2 mapdlsmcl.m ⊢M=mapd⁡K⁡W
3 mapdlsmcl.u ⊢U=DVecH⁡K⁡W
4 mapdlsmcl.c ⊢C=LCDual⁡K⁡W
5 mapdlsmcl.p ⊢⊕˙=LSSum⁡C
6 mapdlsmcl.k ⊢φ→K∈HL∧W∈H
7 mapdlsmcl.x ⊢φ→X∈ran⁡M
8 mapdlsmcl.y ⊢φ→Y∈ran⁡M
9 1 4 6 lcdlmod ⊢φ→C∈LMod
10 eqid ⊢LSubSp⁡C=LSubSp⁡C
11 1 2 4 10 6 mapdrn2 ⊢φ→ran⁡M=LSubSp⁡C
12 7 11 eleqtrd ⊢φ→X∈LSubSp⁡C
13 8 11 eleqtrd ⊢φ→Y∈LSubSp⁡C
14 10 5 lsmcl ⊢C∈LMod∧X∈LSubSp⁡C∧Y∈LSubSp⁡C→X⊕˙Y∈LSubSp⁡C
15 9 12 13 14 syl3anc ⊢φ→X⊕˙Y∈LSubSp⁡C
16 15 11 eleqtrrd ⊢φ→X⊕˙Y∈ran⁡M