| Step |
Hyp |
Ref |
Expression |
| 1 |
|
hgmaprnlem1.h |
|- H = ( LHyp ` K ) |
| 2 |
|
hgmaprnlem1.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 3 |
|
hgmaprnlem1.v |
|- V = ( Base ` U ) |
| 4 |
|
hgmaprnlem1.r |
|- R = ( Scalar ` U ) |
| 5 |
|
hgmaprnlem1.b |
|- B = ( Base ` R ) |
| 6 |
|
hgmaprnlem1.t |
|- .x. = ( .s ` U ) |
| 7 |
|
hgmaprnlem1.o |
|- .0. = ( 0g ` U ) |
| 8 |
|
hgmaprnlem1.c |
|- C = ( ( LCDual ` K ) ` W ) |
| 9 |
|
hgmaprnlem1.d |
|- D = ( Base ` C ) |
| 10 |
|
hgmaprnlem1.p |
|- P = ( Scalar ` C ) |
| 11 |
|
hgmaprnlem1.a |
|- A = ( Base ` P ) |
| 12 |
|
hgmaprnlem1.e |
|- .xb = ( .s ` C ) |
| 13 |
|
hgmaprnlem1.q |
|- Q = ( 0g ` C ) |
| 14 |
|
hgmaprnlem1.s |
|- S = ( ( HDMap ` K ) ` W ) |
| 15 |
|
hgmaprnlem1.g |
|- G = ( ( HGMap ` K ) ` W ) |
| 16 |
|
hgmaprnlem1.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 17 |
|
hgmaprnlem1.z |
|- ( ph -> z e. A ) |
| 18 |
1 2 3 7 16
|
dvh1dim |
|- ( ph -> E. t e. V t =/= .0. ) |
| 19 |
|
eldifsn |
|- ( t e. ( V \ { .0. } ) <-> ( t e. V /\ t =/= .0. ) ) |
| 20 |
16
|
adantr |
|- ( ( ph /\ t e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) ) |
| 21 |
17
|
adantr |
|- ( ( ph /\ t e. ( V \ { .0. } ) ) -> z e. A ) |
| 22 |
|
simpr |
|- ( ( ph /\ t e. ( V \ { .0. } ) ) -> t e. ( V \ { .0. } ) ) |
| 23 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 20 21 22
|
hgmaprnlem4N |
|- ( ( ph /\ t e. ( V \ { .0. } ) ) -> z e. ran G ) |
| 24 |
19 23
|
sylan2br |
|- ( ( ph /\ ( t e. V /\ t =/= .0. ) ) -> z e. ran G ) |
| 25 |
18 24
|
rexlimddv |
|- ( ph -> z e. ran G ) |