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 onto LSubSp ⁡ 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 onto LSubSp ⁡ 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 LSubSp ⁡ 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-1 LSubSp ⁡ 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 onto ran ⁡ M
16 13 14 15 3syl ⊢ φ → M : LSubSp ⁡ DVecH ⁡ K ⁡ W ⟶ 1-1 onto ran ⁡ M
17 f1ocnvfv2 ⊢ M : LSubSp ⁡ DVecH ⁡ K ⁡ W ⟶ 1-1 onto ran ⁡ M ∧ X ∈ ran ⁡ M → M ⁡ M -1 ⁡ X = X
18 16 4 17 syl2anc ⊢ φ → M ⁡ M -1 ⁡ X = X