Step |
Hyp |
Ref |
Expression |
1 |
|
dia1dim.h |
|- H = ( LHyp ` K ) |
2 |
|
dia1dim.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
dia1dim.r |
|- R = ( ( trL ` K ) ` W ) |
4 |
|
dia1dim.e |
|- E = ( ( TEndo ` K ) ` W ) |
5 |
|
dia1dim.i |
|- I = ( ( DIsoA ` K ) ` W ) |
6 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) ) |
7 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
8 |
7 1 2 3
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. ( Base ` K ) ) |
9 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
10 |
9 1 2 3
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W ) |
11 |
7 9 1 2 3 5
|
diaval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. ( Base ` K ) /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } ) |
12 |
6 8 10 11
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } ) |
13 |
9 1 2 3 4
|
dva1dim |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> { g | E. s e. E g = ( s ` F ) } = { g e. T | ( R ` g ) ( le ` K ) ( R ` F ) } ) |
14 |
12 13
|
eqtr4d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g | E. s e. E g = ( s ` F ) } ) |