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 onto LSubSp ⁡ LDual ⁡ U ∩ 𝒫 g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g
14 f1ocnvfv1 ⊢ M : S ⟶ 1-1 onto LSubSp ⁡ 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