Metamath Proof Explorer

Theorem mapdincl

Description: Closure of dual subspace intersection for the map defined by df-mapd . (Contributed by NM, 12-Apr-2015)

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

Proof

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