Metamath Proof Explorer

Theorem mapdcl

Description: Closure the value 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
mapdcl.x ⊢ φ → X ∈ S
Assertion mapdcl ⊢ φ → M ⁡ X ∈ ran ⁡ M

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 f1ofn ⊢ M : S ⟶ 1-1 onto LSubSp ⁡ LDual ⁡ U ∩ 𝒫 g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g → M Fn S
15 13 14 syl ⊢ φ → M Fn S
16 dffn3 ⊢ M Fn S ↔ M : S ⟶ ran ⁡ M
17 15 16 sylib ⊢ φ → M : S ⟶ ran ⁡ M
18 17 6 ffvelrnd ⊢ φ → M ⁡ X ∈ ran ⁡ M