Step |
Hyp |
Ref |
Expression |
1 |
|
dia0.b |
|- B = ( Base ` K ) |
2 |
|
dia0.z |
|- .0. = ( 0. ` K ) |
3 |
|
dia0.h |
|- H = ( LHyp ` K ) |
4 |
|
dia0.i |
|- I = ( ( DIsoA ` K ) ` W ) |
5 |
|
id |
|- ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) ) |
6 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
7 |
1 2
|
atl0cl |
|- ( K e. AtLat -> .0. e. B ) |
8 |
6 7
|
syl |
|- ( K e. HL -> .0. e. B ) |
9 |
8
|
adantr |
|- ( ( K e. HL /\ W e. H ) -> .0. e. B ) |
10 |
1 3
|
lhpbase |
|- ( W e. H -> W e. B ) |
11 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
12 |
1 11 2
|
atl0le |
|- ( ( K e. AtLat /\ W e. B ) -> .0. ( le ` K ) W ) |
13 |
6 10 12
|
syl2an |
|- ( ( K e. HL /\ W e. H ) -> .0. ( le ` K ) W ) |
14 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
15 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
16 |
1 11 3 14 15 4
|
diaval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( .0. e. B /\ .0. ( le ` K ) W ) ) -> ( I ` .0. ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } ) |
17 |
5 9 13 16
|
syl12anc |
|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } ) |
18 |
6
|
ad2antrr |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> K e. AtLat ) |
19 |
1 3 14 15
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` f ) e. B ) |
20 |
1 11 2
|
atlle0 |
|- ( ( K e. AtLat /\ ( ( ( trL ` K ) ` W ) ` f ) e. B ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) ) |
21 |
18 19 20
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) ) |
22 |
1 2 3 14 15
|
trlid0b |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( f = ( _I |` B ) <-> ( ( ( trL ` K ) ` W ) ` f ) = .0. ) ) |
23 |
21 22
|
bitr4d |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. <-> f = ( _I |` B ) ) ) |
24 |
23
|
rabbidva |
|- ( ( K e. HL /\ W e. H ) -> { f e. ( ( LTrn ` K ) ` W ) | ( ( ( trL ` K ) ` W ) ` f ) ( le ` K ) .0. } = { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } ) |
25 |
1 3 14
|
idltrn |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. ( ( LTrn ` K ) ` W ) ) |
26 |
|
rabsn |
|- ( ( _I |` B ) e. ( ( LTrn ` K ) ` W ) -> { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } = { ( _I |` B ) } ) |
27 |
25 26
|
syl |
|- ( ( K e. HL /\ W e. H ) -> { f e. ( ( LTrn ` K ) ` W ) | f = ( _I |` B ) } = { ( _I |` B ) } ) |
28 |
17 24 27
|
3eqtrd |
|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { ( _I |` B ) } ) |