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