| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lcdlkreq.h |
|- H = ( LHyp ` K ) |
| 2 |
|
lcdlkreq.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 3 |
|
lcdlkreq.l |
|- L = ( LKer ` U ) |
| 4 |
|
lcdlkreq.c |
|- C = ( ( LCDual ` K ) ` W ) |
| 5 |
|
lcdlkreq.o |
|- .0. = ( 0g ` C ) |
| 6 |
|
lcdlkreq.n |
|- N = ( LSpan ` C ) |
| 7 |
|
lcdlkreq.v |
|- V = ( Base ` C ) |
| 8 |
|
lcdlkreq.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 9 |
|
lcdlkreq.i |
|- ( ph -> I e. V ) |
| 10 |
|
lcdlkreq.g |
|- ( ph -> G e. ( N ` { I } ) ) |
| 11 |
|
lcdlkreq.z |
|- ( ph -> G =/= .0. ) |
| 12 |
|
eqid |
|- ( LFnl ` U ) = ( LFnl ` U ) |
| 13 |
|
eqid |
|- ( LDual ` U ) = ( LDual ` U ) |
| 14 |
|
eqid |
|- ( 0g ` ( LDual ` U ) ) = ( 0g ` ( LDual ` U ) ) |
| 15 |
|
eqid |
|- ( LSpan ` ( LDual ` U ) ) = ( LSpan ` ( LDual ` U ) ) |
| 16 |
1 2 8
|
dvhlvec |
|- ( ph -> U e. LVec ) |
| 17 |
1 4 7 2 12 8 9
|
lcdvbaselfl |
|- ( ph -> I e. ( LFnl ` U ) ) |
| 18 |
9
|
snssd |
|- ( ph -> { I } C_ V ) |
| 19 |
1 2 13 15 4 7 6 8 18
|
lcdlsp |
|- ( ph -> ( N ` { I } ) = ( ( LSpan ` ( LDual ` U ) ) ` { I } ) ) |
| 20 |
10 19
|
eleqtrd |
|- ( ph -> G e. ( ( LSpan ` ( LDual ` U ) ) ` { I } ) ) |
| 21 |
1 2 13 14 4 5 8
|
lcd0v2 |
|- ( ph -> .0. = ( 0g ` ( LDual ` U ) ) ) |
| 22 |
11 21
|
neeqtrd |
|- ( ph -> G =/= ( 0g ` ( LDual ` U ) ) ) |
| 23 |
|
eldifsn |
|- ( G e. ( ( ( LSpan ` ( LDual ` U ) ) ` { I } ) \ { ( 0g ` ( LDual ` U ) ) } ) <-> ( G e. ( ( LSpan ` ( LDual ` U ) ) ` { I } ) /\ G =/= ( 0g ` ( LDual ` U ) ) ) ) |
| 24 |
20 22 23
|
sylanbrc |
|- ( ph -> G e. ( ( ( LSpan ` ( LDual ` U ) ) ` { I } ) \ { ( 0g ` ( LDual ` U ) ) } ) ) |
| 25 |
12 3 13 14 15 16 17 24
|
lkrlspeqN |
|- ( ph -> ( L ` G ) = ( L ` I ) ) |