Description: Lemma for hdmaprnN . TODO: This lemma doesn't quite pay for itself even though used six times. Maybe prove this directly instead. (Contributed by NM, 27-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 ) |
||
| hdmaprnlem1.t2 | |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) ) |
||
| Assertion | hdmaprnlem4tN | |- ( ph -> t e. V ) |
| 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 | hdmaprnlem1.t2 | |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) ) |
|
| 20 | 1 2 9 | dvhlmod | |- ( ph -> U e. LMod ) |
| 21 | 11 | snssd | |- ( ph -> { v } C_ V ) |
| 22 | 3 4 | lspssv | |- ( ( U e. LMod /\ { v } C_ V ) -> ( N ` { v } ) C_ V ) |
| 23 | 20 21 22 | syl2anc | |- ( ph -> ( N ` { v } ) C_ V ) |
| 24 | 23 | ssdifssd | |- ( ph -> ( ( N ` { v } ) \ { .0. } ) C_ V ) |
| 25 | 24 19 | sseldd | |- ( ph -> t e. V ) |