Metamath Proof Explorer

Theorem mapddlssN

Description: The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 instead. (Contributed by NM, 31-Jan-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapddlss.h ⊢ H = LHyp ⁡ K
mapddlss.m ⊢ M = mapd ⁡ K ⁡ W
mapddlss.u ⊢ U = DVecH ⁡ K ⁡ W
mapddlss.s ⊢ S = LSubSp ⁡ U
mapddlss.d ⊢ D = LDual ⁡ U
mapddlss.t ⊢ T = LSubSp ⁡ D
mapddlss.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapddlss.r ⊢ φ → R ∈ S
Assertion mapddlssN ⊢ φ → M ⁡ R ∈ T

Proof

Step Hyp Ref Expression
1 mapddlss.h ⊢ H = LHyp ⁡ K
2 mapddlss.m ⊢ M = mapd ⁡ K ⁡ W
3 mapddlss.u ⊢ U = DVecH ⁡ K ⁡ W
4 mapddlss.s ⊢ S = LSubSp ⁡ U
5 mapddlss.d ⊢ D = LDual ⁡ U
6 mapddlss.t ⊢ T = LSubSp ⁡ D
7 mapddlss.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 mapddlss.r ⊢ φ → R ∈ S
9 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
10 eqid ⊢ LKer ⁡ U = LKer ⁡ U
11 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
12 1 3 4 9 10 11 2 7 8 mapdval ⊢ φ → M ⁡ R = f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∧ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f ⊆ R
13 eqid ⊢ f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∧ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f ⊆ R = f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∧ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f ⊆ R
14 1 11 3 4 9 10 5 6 13 7 8 lclkrs ⊢ φ → f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∧ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f ⊆ R ∈ T
15 12 14 eqeltrd ⊢ φ → M ⁡ R ∈ T