| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mapdpg.h |
|- H = ( LHyp ` K ) |
| 2 |
|
mapdpg.m |
|- M = ( ( mapd ` K ) ` W ) |
| 3 |
|
mapdpg.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 4 |
|
mapdpg.v |
|- V = ( Base ` U ) |
| 5 |
|
mapdpg.s |
|- .- = ( -g ` U ) |
| 6 |
|
mapdpg.z |
|- .0. = ( 0g ` U ) |
| 7 |
|
mapdpg.n |
|- N = ( LSpan ` U ) |
| 8 |
|
mapdpg.c |
|- C = ( ( LCDual ` K ) ` W ) |
| 9 |
|
mapdpg.f |
|- F = ( Base ` C ) |
| 10 |
|
mapdpg.r |
|- R = ( -g ` C ) |
| 11 |
|
mapdpg.j |
|- J = ( LSpan ` C ) |
| 12 |
|
mapdpg.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 13 |
|
mapdpg.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
| 14 |
|
mapdpg.y |
|- ( ph -> Y e. ( V \ { .0. } ) ) |
| 15 |
|
mapdpg.g |
|- ( ph -> G e. F ) |
| 16 |
|
mapdpg.ne |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
| 17 |
|
mapdpg.e |
|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { G } ) ) |
| 18 |
|
eqid |
|- ( LSAtoms ` U ) = ( LSAtoms ` U ) |
| 19 |
|
eqid |
|- ( LSAtoms ` C ) = ( LSAtoms ` C ) |
| 20 |
1 3 12
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 21 |
4 7 6 18 20 13
|
lsatlspsn |
|- ( ph -> ( N ` { X } ) e. ( LSAtoms ` U ) ) |
| 22 |
1 2 3 18 8 19 12 21
|
mapdat |
|- ( ph -> ( M ` ( N ` { X } ) ) e. ( LSAtoms ` C ) ) |
| 23 |
17 22
|
eqeltrrd |
|- ( ph -> ( J ` { G } ) e. ( LSAtoms ` C ) ) |
| 24 |
|
eqid |
|- ( 0g ` C ) = ( 0g ` C ) |
| 25 |
1 8 12
|
lcdlmod |
|- ( ph -> C e. LMod ) |
| 26 |
9 11 24 19 25 15
|
lsatspn0 |
|- ( ph -> ( ( J ` { G } ) e. ( LSAtoms ` C ) <-> G =/= ( 0g ` C ) ) ) |
| 27 |
23 26
|
mpbid |
|- ( ph -> G =/= ( 0g ` C ) ) |