Description: Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hvmap1o2.h | |- H = ( LHyp ` K ) |
|
hvmap1o2.u | |- U = ( ( DVecH ` K ) ` W ) |
||
hvmap1o2.v | |- V = ( Base ` U ) |
||
hvmap1o2.z | |- .0. = ( 0g ` U ) |
||
hvmap1o2.c | |- C = ( ( LCDual ` K ) ` W ) |
||
hvmap1o2.f | |- F = ( Base ` C ) |
||
hvmap1o2.o | |- O = ( 0g ` C ) |
||
hvmap1o2.m | |- M = ( ( HVMap ` K ) ` W ) |
||
hvmap1o2.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
hvmapcl2.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
||
Assertion | hvmapcl2 | |- ( ph -> ( M ` X ) e. ( F \ { O } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hvmap1o2.h | |- H = ( LHyp ` K ) |
|
2 | hvmap1o2.u | |- U = ( ( DVecH ` K ) ` W ) |
|
3 | hvmap1o2.v | |- V = ( Base ` U ) |
|
4 | hvmap1o2.z | |- .0. = ( 0g ` U ) |
|
5 | hvmap1o2.c | |- C = ( ( LCDual ` K ) ` W ) |
|
6 | hvmap1o2.f | |- F = ( Base ` C ) |
|
7 | hvmap1o2.o | |- O = ( 0g ` C ) |
|
8 | hvmap1o2.m | |- M = ( ( HVMap ` K ) ` W ) |
|
9 | hvmap1o2.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
10 | hvmapcl2.x | |- ( ph -> X e. ( V \ { .0. } ) ) |
|
11 | 1 2 3 4 5 6 7 8 9 | hvmap1o2 | |- ( ph -> M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) ) |
12 | f1of | |- ( M : ( V \ { .0. } ) -1-1-onto-> ( F \ { O } ) -> M : ( V \ { .0. } ) --> ( F \ { O } ) ) |
|
13 | 11 12 | syl | |- ( ph -> M : ( V \ { .0. } ) --> ( F \ { O } ) ) |
14 | 13 10 | ffvelrnd | |- ( ph -> ( M ` X ) e. ( F \ { O } ) ) |