| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lcdlss.h |
|- H = ( LHyp ` K ) |
| 2 |
|
lcdlss.o |
|- O = ( ( ocH ` K ) ` W ) |
| 3 |
|
lcdlss.c |
|- C = ( ( LCDual ` K ) ` W ) |
| 4 |
|
lcdlss.s |
|- S = ( LSubSp ` C ) |
| 5 |
|
lcdlss.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 6 |
|
lcdlss.f |
|- F = ( LFnl ` U ) |
| 7 |
|
lcdlss.l |
|- L = ( LKer ` U ) |
| 8 |
|
lcdlss.d |
|- D = ( LDual ` U ) |
| 9 |
|
lcdlss.t |
|- T = ( LSubSp ` D ) |
| 10 |
|
lcdlss.b |
|- B = { f e. F | ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) } |
| 11 |
|
lcdlss.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 12 |
1 2 3 5 6 7 8 11 10
|
lcdval2 |
|- ( ph -> C = ( D |`s B ) ) |
| 13 |
12
|
fveq2d |
|- ( ph -> ( LSubSp ` C ) = ( LSubSp ` ( D |`s B ) ) ) |
| 14 |
4 13
|
syl5eq |
|- ( ph -> S = ( LSubSp ` ( D |`s B ) ) ) |
| 15 |
14
|
eleq2d |
|- ( ph -> ( u e. S <-> u e. ( LSubSp ` ( D |`s B ) ) ) ) |
| 16 |
1 5 11
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 17 |
8 16
|
lduallmod |
|- ( ph -> D e. LMod ) |
| 18 |
1 5 2 6 7 8 9 10 11
|
lclkr |
|- ( ph -> B e. T ) |
| 19 |
|
eqid |
|- ( D |`s B ) = ( D |`s B ) |
| 20 |
|
eqid |
|- ( LSubSp ` ( D |`s B ) ) = ( LSubSp ` ( D |`s B ) ) |
| 21 |
19 9 20
|
lsslss |
|- ( ( D e. LMod /\ B e. T ) -> ( u e. ( LSubSp ` ( D |`s B ) ) <-> ( u e. T /\ u C_ B ) ) ) |
| 22 |
17 18 21
|
syl2anc |
|- ( ph -> ( u e. ( LSubSp ` ( D |`s B ) ) <-> ( u e. T /\ u C_ B ) ) ) |
| 23 |
15 22
|
bitrd |
|- ( ph -> ( u e. S <-> ( u e. T /\ u C_ B ) ) ) |
| 24 |
|
elin |
|- ( u e. ( T i^i ~P B ) <-> ( u e. T /\ u e. ~P B ) ) |
| 25 |
|
velpw |
|- ( u e. ~P B <-> u C_ B ) |
| 26 |
25
|
anbi2i |
|- ( ( u e. T /\ u e. ~P B ) <-> ( u e. T /\ u C_ B ) ) |
| 27 |
24 26
|
bitr2i |
|- ( ( u e. T /\ u C_ B ) <-> u e. ( T i^i ~P B ) ) |
| 28 |
23 27
|
bitrdi |
|- ( ph -> ( u e. S <-> u e. ( T i^i ~P B ) ) ) |
| 29 |
28
|
eqrdv |
|- ( ph -> S = ( T i^i ~P B ) ) |