# 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}=\mathrm{LHyp}\left({K}\right)$
mapdcnvcl.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdcnvcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdcnvcl.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
mapdcnvcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdcnvcl.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{M}$
Assertion mapdcnvcl ${⊢}{\phi }\to {{M}}^{-1}\left({X}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 mapdcnvcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdcnvcl.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdcnvcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdcnvcl.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
5 mapdcnvcl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 mapdcnvcl.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{M}$
7 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
8 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
9 eqid ${⊢}\mathrm{LKer}\left({U}\right)=\mathrm{LKer}\left({U}\right)$
10 eqid ${⊢}\mathrm{LDual}\left({U}\right)=\mathrm{LDual}\left({U}\right)$
11 eqid ${⊢}\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)=\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)$
12 eqid ${⊢}\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}=\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}$
13 1 7 2 3 4 8 9 10 11 12 5 mapd1o ${⊢}{\phi }\to {M}:{S}\underset{1-1 onto}{⟶}\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)\cap 𝒫\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}$
14 f1of1 ${⊢}{M}:{S}\underset{1-1 onto}{⟶}\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)\cap 𝒫\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}\to {M}:{S}\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)\cap 𝒫\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}$
15 f1f1orn ${⊢}{M}:{S}\underset{1-1}{⟶}\mathrm{LSubSp}\left(\mathrm{LDual}\left({U}\right)\right)\cap 𝒫\left\{{g}\in \mathrm{LFnl}\left({U}\right)|\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{LKer}\left({U}\right)\left({g}\right)\right)\right)=\mathrm{LKer}\left({U}\right)\left({g}\right)\right\}\to {M}:{S}\underset{1-1 onto}{⟶}\mathrm{ran}{M}$
16 13 14 15 3syl ${⊢}{\phi }\to {M}:{S}\underset{1-1 onto}{⟶}\mathrm{ran}{M}$
17 f1ocnvdm ${⊢}\left({M}:{S}\underset{1-1 onto}{⟶}\mathrm{ran}{M}\wedge {X}\in \mathrm{ran}{M}\right)\to {{M}}^{-1}\left({X}\right)\in {S}$
18 16 6 17 syl2anc ${⊢}{\phi }\to {{M}}^{-1}\left({X}\right)\in {S}$