Metamath Proof Explorer

Theorem mapdcnvcl

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

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

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 mapdcnvcl.x ⊢ φ → X ∈ ran ⁡ M
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 f1of1 ⊢ M : S ⟶ 1-1 onto LSubSp ⁡ LDual ⁡ U ∩ 𝒫 g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g → M : S ⟶ 1-1 LSubSp ⁡ LDual ⁡ U ∩ 𝒫 g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g
15 f1f1orn ⊢ M : S ⟶ 1-1 LSubSp ⁡ LDual ⁡ U ∩ 𝒫 g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g → M : S ⟶ 1-1 onto ran ⁡ M
16 13 14 15 3syl ⊢ φ → M : S ⟶ 1-1 onto ran ⁡ M
17 f1ocnvdm ⊢ M : S ⟶ 1-1 onto ran ⁡ M ∧ X ∈ ran ⁡ M → M -1 ⁡ X ∈ S
18 16 6 17 syl2anc ⊢ φ → M -1 ⁡ X ∈ S