# Metamath Proof Explorer

## Theorem mapdcnvid1N

Description: Converse of the value of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

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)$
mapdcl.x ${⊢}{\phi }\to {X}\in {S}$
Assertion mapdcnvid1N ${⊢}{\phi }\to {{M}}^{-1}\left({M}\left({X}\right)\right)={X}$

### 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 mapdcl.x ${⊢}{\phi }\to {X}\in {S}$
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 f1ocnvfv1 ${⊢}\left({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\}\wedge {X}\in {S}\right)\to {{M}}^{-1}\left({M}\left({X}\right)\right)={X}$
15 13 6 14 syl2anc ${⊢}{\phi }\to {{M}}^{-1}\left({M}\left({X}\right)\right)={X}$