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