Metamath Proof Explorer

Theorem mapdrn2

Description: Range of the map defined by df-mapd . TODO: this seems to be needed a lot in hdmaprnlem3eN etc. Would it be better to change df-mapd theorems to use LSubSpC instead of ran M ? (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses mapdrn2.h ⊢ H = LHyp ⁡ K
mapdrn2.m ⊢ M = mapd ⁡ K ⁡ W
mapdrn2.c ⊢ C = LCDual ⁡ K ⁡ W
mapdrn2.t ⊢ T = LSubSp ⁡ C
mapdrn2.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion mapdrn2 ⊢ φ → ran ⁡ M = T

Proof

Step Hyp Ref Expression
1 mapdrn2.h ⊢ H = LHyp ⁡ K
2 mapdrn2.m ⊢ M = mapd ⁡ K ⁡ W
3 mapdrn2.c ⊢ C = LCDual ⁡ K ⁡ W
4 mapdrn2.t ⊢ T = LSubSp ⁡ C
5 mapdrn2.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
7 eqid ⊢ DVecH ⁡ K ⁡ W = 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 ⊢ f ∈ LFnl ⁡ DVecH ⁡ K ⁡ W | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f = f ∈ LFnl ⁡ DVecH ⁡ K ⁡ W | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f
13 1 6 2 7 8 9 10 11 12 5 mapdrn ⊢ φ → ran ⁡ M = LSubSp ⁡ LDual ⁡ DVecH ⁡ K ⁡ W ∩ 𝒫 f ∈ LFnl ⁡ DVecH ⁡ K ⁡ W | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f
14 1 6 3 4 7 8 9 10 11 12 5 lcdlss ⊢ φ → T = LSubSp ⁡ LDual ⁡ DVecH ⁡ K ⁡ W ∩ 𝒫 f ∈ LFnl ⁡ DVecH ⁡ K ⁡ W | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ W ⁡ f
15 13 14 eqtr4d ⊢ φ → ran ⁡ M = T