Step |
Hyp |
Ref |
Expression |
1 |
|
ldilval.b |
|- B = ( Base ` K ) |
2 |
|
ldilval.l |
|- .<_ = ( le ` K ) |
3 |
|
ldilval.h |
|- H = ( LHyp ` K ) |
4 |
|
ldilval.d |
|- D = ( ( LDil ` K ) ` W ) |
5 |
|
eqid |
|- ( LAut ` K ) = ( LAut ` K ) |
6 |
1 2 3 5 4
|
isldil |
|- ( ( K e. V /\ W e. H ) -> ( F e. D <-> ( F e. ( LAut ` K ) /\ A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) ) ) |
7 |
|
simpr |
|- ( ( F e. ( LAut ` K ) /\ A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) -> A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) |
8 |
6 7
|
syl6bi |
|- ( ( K e. V /\ W e. H ) -> ( F e. D -> A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) ) |
9 |
|
breq1 |
|- ( x = X -> ( x .<_ W <-> X .<_ W ) ) |
10 |
|
fveq2 |
|- ( x = X -> ( F ` x ) = ( F ` X ) ) |
11 |
|
id |
|- ( x = X -> x = X ) |
12 |
10 11
|
eqeq12d |
|- ( x = X -> ( ( F ` x ) = x <-> ( F ` X ) = X ) ) |
13 |
9 12
|
imbi12d |
|- ( x = X -> ( ( x .<_ W -> ( F ` x ) = x ) <-> ( X .<_ W -> ( F ` X ) = X ) ) ) |
14 |
13
|
rspccv |
|- ( A. x e. B ( x .<_ W -> ( F ` x ) = x ) -> ( X e. B -> ( X .<_ W -> ( F ` X ) = X ) ) ) |
15 |
14
|
impd |
|- ( A. x e. B ( x .<_ W -> ( F ` x ) = x ) -> ( ( X e. B /\ X .<_ W ) -> ( F ` X ) = X ) ) |
16 |
8 15
|
syl6 |
|- ( ( K e. V /\ W e. H ) -> ( F e. D -> ( ( X e. B /\ X .<_ W ) -> ( F ` X ) = X ) ) ) |
17 |
16
|
3imp |
|- ( ( ( K e. V /\ W e. H ) /\ F e. D /\ ( X e. B /\ X .<_ W ) ) -> ( F ` X ) = X ) |