Description: Lemma for hdmaprnN . Show s is in the range of S . (Contributed by NM, 29-May-2015) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hdmaprnlem1.h | |- H = ( LHyp ` K ) |
|
| hdmaprnlem1.u | |- U = ( ( DVecH ` K ) ` W ) |
||
| hdmaprnlem1.v | |- V = ( Base ` U ) |
||
| hdmaprnlem1.n | |- N = ( LSpan ` U ) |
||
| hdmaprnlem1.c | |- C = ( ( LCDual ` K ) ` W ) |
||
| hdmaprnlem1.l | |- L = ( LSpan ` C ) |
||
| hdmaprnlem1.m | |- M = ( ( mapd ` K ) ` W ) |
||
| hdmaprnlem1.s | |- S = ( ( HDMap ` K ) ` W ) |
||
| hdmaprnlem1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| hdmaprnlem1.se | |- ( ph -> s e. ( D \ { Q } ) ) |
||
| hdmaprnlem1.ve | |- ( ph -> v e. V ) |
||
| hdmaprnlem1.e | |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) |
||
| hdmaprnlem1.ue | |- ( ph -> u e. V ) |
||
| hdmaprnlem1.un | |- ( ph -> -. u e. ( N ` { v } ) ) |
||
| hdmaprnlem1.d | |- D = ( Base ` C ) |
||
| hdmaprnlem1.q | |- Q = ( 0g ` C ) |
||
| hdmaprnlem1.o | |- .0. = ( 0g ` U ) |
||
| hdmaprnlem1.a | |- .+b = ( +g ` C ) |
||
| hdmaprnlem3e.p | |- .+ = ( +g ` U ) |
||
| Assertion | hdmaprnlem11N | |- ( ph -> s e. ran S ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hdmaprnlem1.h | |- H = ( LHyp ` K ) |
|
| 2 | hdmaprnlem1.u | |- U = ( ( DVecH ` K ) ` W ) |
|
| 3 | hdmaprnlem1.v | |- V = ( Base ` U ) |
|
| 4 | hdmaprnlem1.n | |- N = ( LSpan ` U ) |
|
| 5 | hdmaprnlem1.c | |- C = ( ( LCDual ` K ) ` W ) |
|
| 6 | hdmaprnlem1.l | |- L = ( LSpan ` C ) |
|
| 7 | hdmaprnlem1.m | |- M = ( ( mapd ` K ) ` W ) |
|
| 8 | hdmaprnlem1.s | |- S = ( ( HDMap ` K ) ` W ) |
|
| 9 | hdmaprnlem1.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 10 | hdmaprnlem1.se | |- ( ph -> s e. ( D \ { Q } ) ) |
|
| 11 | hdmaprnlem1.ve | |- ( ph -> v e. V ) |
|
| 12 | hdmaprnlem1.e | |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) ) |
|
| 13 | hdmaprnlem1.ue | |- ( ph -> u e. V ) |
|
| 14 | hdmaprnlem1.un | |- ( ph -> -. u e. ( N ` { v } ) ) |
|
| 15 | hdmaprnlem1.d | |- D = ( Base ` C ) |
|
| 16 | hdmaprnlem1.q | |- Q = ( 0g ` C ) |
|
| 17 | hdmaprnlem1.o | |- .0. = ( 0g ` U ) |
|
| 18 | hdmaprnlem1.a | |- .+b = ( +g ` C ) |
|
| 19 | hdmaprnlem3e.p | |- .+ = ( +g ` U ) |
|
| 20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 | hdmaprnlem10N | |- ( ph -> E. t e. V ( S ` t ) = s ) |
| 21 | 1 2 3 8 9 | hdmapfnN | |- ( ph -> S Fn V ) |
| 22 | fvelrnb | |- ( S Fn V -> ( s e. ran S <-> E. t e. V ( S ` t ) = s ) ) |
|
| 23 | 21 22 | syl | |- ( ph -> ( s e. ran S <-> E. t e. V ( S ` t ) = s ) ) |
| 24 | 20 23 | mpbird | |- ( ph -> s e. ran S ) |