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 |
1 2 3 5
|
diasslssN |
|- ( ( K e. HL /\ W e. H ) -> ran I C_ S ) |
7 |
|
sseqin2 |
|- ( ran I C_ S <-> ( S i^i ran I ) = ran I ) |
8 |
6 7
|
sylib |
|- ( ( K e. HL /\ W e. H ) -> ( S i^i ran I ) = ran I ) |
9 |
1 3 4
|
doca3N |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. ran I ) -> ( ._|_ ` ( ._|_ ` x ) ) = x ) |
10 |
9
|
ex |
|- ( ( K e. HL /\ W e. H ) -> ( x e. ran I -> ( ._|_ ` ( ._|_ ` x ) ) = x ) ) |
11 |
10
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. S ) -> ( x e. ran I -> ( ._|_ ` ( ._|_ ` x ) ) = x ) ) |
12 |
1 2 3 4 5
|
dvadiaN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( x e. S /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) -> x e. ran I ) |
13 |
12
|
expr |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. S ) -> ( ( ._|_ ` ( ._|_ ` x ) ) = x -> x e. ran I ) ) |
14 |
11 13
|
impbid |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. S ) -> ( x e. ran I <-> ( ._|_ ` ( ._|_ ` x ) ) = x ) ) |
15 |
14
|
rabbi2dva |
|- ( ( K e. HL /\ W e. H ) -> ( S i^i ran I ) = { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } ) |
16 |
8 15
|
eqtr3d |
|- ( ( K e. HL /\ W e. H ) -> ran I = { x e. S | ( ._|_ ` ( ._|_ ` x ) ) = x } ) |