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