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=LHyp⁡K
mapdcnvid2.m ⊢M=mapd⁡K⁡W
mapdcnvid2.k ⊢φ→K∈HL∧W∈H
mapdcnvid2.x ⊢φ→X∈ran⁡M
Assertion mapdcnvid2 ⊢φ→M⁡M-1⁡X=X

Proof

Step Hyp Ref Expression
1 mapdcnvid2.h ⊢H=LHyp⁡K
2 mapdcnvid2.m ⊢M=mapd⁡K⁡W
3 mapdcnvid2.k ⊢φ→K∈HL∧W∈H
4 mapdcnvid2.x ⊢φ→X∈ran⁡M
5 eqid ⊢ocH⁡K⁡W=ocH⁡K⁡W
6 eqid ⊢DVecH⁡K⁡W=DVecH⁡K⁡W
7 eqid ⊢LSubSp⁡DVecH⁡K⁡W=LSubSp⁡DVecH⁡K⁡W
8 eqid ⊢LFnl⁡DVecH⁡K⁡W=LFnl⁡DVecH⁡K⁡W
9 eqid ⊢LKer⁡DVecH⁡K⁡W=LKer⁡DVecH⁡K⁡W
10 eqid ⊢LDual⁡DVecH⁡K⁡W=LDual⁡DVecH⁡K⁡W
11 eqid ⊢LSubSp⁡LDual⁡DVecH⁡K⁡W=LSubSp⁡LDual⁡DVecH⁡K⁡W
12 eqid ⊢g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g=g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g
13 1 5 2 6 7 8 9 10 11 12 3 mapd1o ⊢φ→M:LSubSp⁡DVecH⁡K⁡W⟶1-1 ontoLSubSp⁡LDual⁡DVecH⁡K⁡W∩𝒫g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g
14 f1of1 ⊢M:LSubSp⁡DVecH⁡K⁡W⟶1-1 ontoLSubSp⁡LDual⁡DVecH⁡K⁡W∩𝒫g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g→M:LSubSp⁡DVecH⁡K⁡W⟶1-1LSubSp⁡LDual⁡DVecH⁡K⁡W∩𝒫g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g
15 f1f1orn ⊢M:LSubSp⁡DVecH⁡K⁡W⟶1-1LSubSp⁡LDual⁡DVecH⁡K⁡W∩𝒫g∈LFnl⁡DVecH⁡K⁡W|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡DVecH⁡K⁡W⁡g=LKer⁡DVecH⁡K⁡W⁡g→M:LSubSp⁡DVecH⁡K⁡W⟶1-1 ontoran⁡M
16 13 14 15 3syl ⊢φ→M:LSubSp⁡DVecH⁡K⁡W⟶1-1 ontoran⁡M
17 f1ocnvfv2 ⊢M:LSubSp⁡DVecH⁡K⁡W⟶1-1 ontoran⁡M∧X∈ran⁡M→M⁡M-1⁡X=X
18 16 4 17 syl2anc ⊢φ→M⁡M-1⁡X=X