Metamath Proof Explorer


Theorem mapdrn

Description: Range of the map defined by df-mapd . (Contributed by NM, 12-Mar-2015)

Ref Expression
Hypotheses mapdrn.h H = LHyp K
mapdrn.o O = ocH K W
mapdrn.m M = mapd K W
mapdrn.u U = DVecH K W
mapdrn.f F = LFnl U
mapdrn.l L = LKer U
mapdrn.d D = LDual U
mapdrn.t T = LSubSp D
mapdrn.c C = g F | O O L g = L g
mapdrn.k φ K HL W H
Assertion mapdrn φ ran M = T 𝒫 C

Proof

Step Hyp Ref Expression
1 mapdrn.h H = LHyp K
2 mapdrn.o O = ocH K W
3 mapdrn.m M = mapd K W
4 mapdrn.u U = DVecH K W
5 mapdrn.f F = LFnl U
6 mapdrn.l L = LKer U
7 mapdrn.d D = LDual U
8 mapdrn.t T = LSubSp D
9 mapdrn.c C = g F | O O L g = L g
10 mapdrn.k φ K HL W H
11 eqid LSubSp U = LSubSp U
12 1 2 3 4 11 5 6 7 8 9 10 mapd1o φ M : LSubSp U 1-1 onto T 𝒫 C
13 f1ofo M : LSubSp U 1-1 onto T 𝒫 C M : LSubSp U onto T 𝒫 C
14 forn M : LSubSp U onto T 𝒫 C ran M = T 𝒫 C
15 12 13 14 3syl φ ran M = T 𝒫 C