Step |
Hyp |
Ref |
Expression |
1 |
|
dvadia.h |
|- H = ( LHyp ` K ) |
2 |
|
dvadia.u |
|- U = ( ( DVecA ` K ) ` W ) |
3 |
|
dvadia.i |
|- I = ( ( DIsoA ` K ) ` W ) |
4 |
|
dvadia.n |
|- ._|_ = ( ( ocA ` K ) ` W ) |
5 |
|
dvadia.s |
|- S = ( LSubSp ` U ) |
6 |
|
simprr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = X ) |
7 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
8 |
7 5
|
lssss |
|- ( X e. S -> X C_ ( Base ` U ) ) |
9 |
8
|
ad2antrl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> X C_ ( Base ` U ) ) |
10 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
11 |
1 10 2 7
|
dvavbase |
|- ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( LTrn ` K ) ` W ) ) |
12 |
11
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> ( Base ` U ) = ( ( LTrn ` K ) ` W ) ) |
13 |
9 12
|
sseqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> X C_ ( ( LTrn ` K ) ` W ) ) |
14 |
1 10 3 4
|
docaclN |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ ( ( LTrn ` K ) ` W ) ) -> ( ._|_ ` X ) e. ran I ) |
15 |
13 14
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> ( ._|_ ` X ) e. ran I ) |
16 |
1 10 3
|
diaelrnN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ran I ) -> ( ._|_ ` X ) C_ ( ( LTrn ` K ) ` W ) ) |
17 |
15 16
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> ( ._|_ ` X ) C_ ( ( LTrn ` K ) ` W ) ) |
18 |
1 10 3 4
|
docaclN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ ( ( LTrn ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran I ) |
19 |
17 18
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran I ) |
20 |
6 19
|
eqeltrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. S /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) -> X e. ran I ) |