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=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
mapdcl.x ⊢φ→X∈S
Assertion mapdcnvid1N ⊢φ→M-1⁡M⁡X=X

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 mapdcl.x ⊢φ→X∈S
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 f1ocnvfv1 ⊢M:S⟶1-1 ontoLSubSp⁡LDual⁡U∩𝒫g∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡g=LKer⁡U⁡g∧X∈S→M-1⁡M⁡X=X
15 13 6 14 syl2anc ⊢φ→M-1⁡M⁡X=X