Metamath Proof Explorer

Theorem mapdcl

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

Ref Expression
Hypotheses mapdcnvcl.h ⊢H=LHyp⁡K
mapdcnvcl.m ⊢M=mapd⁡K⁡W
mapdcnvcl.u ⊢U=DVecH⁡K⁡W
mapdcnvcl.s ⊢S=LSubSp⁡U
mapdcnvcl.k ⊢φ→K∈HL∧W∈H
mapdcl.x ⊢φ→X∈S
Assertion mapdcl ⊢φ→M⁡X∈ran⁡M

Proof

Step Hyp Ref Expression
1 mapdcnvcl.h ⊢H=LHyp⁡K
2 mapdcnvcl.m ⊢M=mapd⁡K⁡W
3 mapdcnvcl.u ⊢U=DVecH⁡K⁡W
4 mapdcnvcl.s ⊢S=LSubSp⁡U
5 mapdcnvcl.k ⊢φ→K∈HL∧W∈H
6 mapdcl.x ⊢φ→X∈S
7 eqid ⊢ocH⁡K⁡W=ocH⁡K⁡W
8 eqid ⊢LFnl⁡U=LFnl⁡U
9 eqid ⊢LKer⁡U=LKer⁡U
10 eqid ⊢LDual⁡U=LDual⁡U
11 eqid ⊢LSubSp⁡LDual⁡U=LSubSp⁡LDual⁡U
12 eqid ⊢g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g=g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g
13 1 7 2 3 4 8 9 10 11 12 5 mapd1o ⊢φ→M:S⟶1-1 ontoLSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g
14 f1ofn ⊢M:S⟶1-1 ontoLSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g→MFnS
15 13 14 syl ⊢φ→MFnS
16 dffn3 ⊢MFnS↔M:S⟶ran⁡M
17 15 16 sylib ⊢φ→M:S⟶ran⁡M
18 17 6 ffvelcdmd ⊢φ→M⁡X∈ran⁡M