| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dia1dimid.h |
|- H = ( LHyp ` K ) |
| 2 |
|
dia1dimid.t |
|- T = ( ( LTrn ` K ) ` W ) |
| 3 |
|
dia1dimid.r |
|- R = ( ( trL ` K ) ` W ) |
| 4 |
|
dia1dimid.i |
|- I = ( ( DIsoA ` K ) ` W ) |
| 5 |
|
eqid |
|- ( ( DVecA ` K ) ` W ) = ( ( DVecA ` K ) ` W ) |
| 6 |
1 5
|
dvalvec |
|- ( ( K e. HL /\ W e. H ) -> ( ( DVecA ` K ) ` W ) e. LVec ) |
| 7 |
|
lveclmod |
|- ( ( ( DVecA ` K ) ` W ) e. LVec -> ( ( DVecA ` K ) ` W ) e. LMod ) |
| 8 |
6 7
|
syl |
|- ( ( K e. HL /\ W e. H ) -> ( ( DVecA ` K ) ` W ) e. LMod ) |
| 9 |
8
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( DVecA ` K ) ` W ) e. LMod ) |
| 10 |
|
eqid |
|- ( Base ` ( ( DVecA ` K ) ` W ) ) = ( Base ` ( ( DVecA ` K ) ` W ) ) |
| 11 |
1 2 5 10
|
dvavbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecA ` K ) ` W ) ) = T ) |
| 12 |
11
|
eleq2d |
|- ( ( K e. HL /\ W e. H ) -> ( F e. ( Base ` ( ( DVecA ` K ) ` W ) ) <-> F e. T ) ) |
| 13 |
12
|
biimpar |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( Base ` ( ( DVecA ` K ) ` W ) ) ) |
| 14 |
|
eqid |
|- ( LSpan ` ( ( DVecA ` K ) ` W ) ) = ( LSpan ` ( ( DVecA ` K ) ` W ) ) |
| 15 |
10 14
|
lspsnid |
|- ( ( ( ( DVecA ` K ) ` W ) e. LMod /\ F e. ( Base ` ( ( DVecA ` K ) ` W ) ) ) -> F e. ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) ) |
| 16 |
9 13 15
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) ) |
| 17 |
1 2 3 5 4 14
|
dia1dim2 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( LSpan ` ( ( DVecA ` K ) ` W ) ) ` { F } ) ) |
| 18 |
16 17
|
eleqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F e. ( I ` ( R ` F ) ) ) |