# Metamath Proof Explorer

## Theorem mapdcnvid2

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

Ref Expression
Hypotheses mapdcnvid2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdcnvid2.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdcnvid2.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdcnvid2.x ${⊢}{\phi }\to {X}\in \mathrm{ran}{M}$
Assertion mapdcnvid2 ${⊢}{\phi }\to {M}\left({{M}}^{-1}\left({X}\right)\right)={X}$

### Proof

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