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