Metamath Proof Explorer

Theorem mapdcnvcl

Description: Closure of the converse 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
mapdcnvcl.x ⊢φ→X∈ran⁡M
Assertion mapdcnvcl ⊢φ→M-1⁡X∈S

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 mapdcnvcl.x ⊢φ→X∈ran⁡M
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 f1of1 ⊢M:S⟶1-1 ontoLSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g→M:S⟶1-1LSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g
15 f1f1orn ⊢M:S⟶1-1LSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g→M:S⟶1-1 ontoran⁡M
16 13 14 15 3syl ⊢φ→M:S⟶1-1 ontoran⁡M
17 f1ocnvdm ⊢M:S⟶1-1 ontoran⁡M∧X∈ran⁡M→M-1⁡X∈S
18 16 6 17 syl2anc ⊢φ→M-1⁡X∈S