Step |
Hyp |
Ref |
Expression |
1 |
|
diaval.b |
|- B = ( Base ` K ) |
2 |
|
diaval.l |
|- .<_ = ( le ` K ) |
3 |
|
diaval.h |
|- H = ( LHyp ` K ) |
4 |
|
diaval.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
diaval.r |
|- R = ( ( trL ` K ) ` W ) |
6 |
|
diaval.i |
|- I = ( ( DIsoA ` K ) ` W ) |
7 |
1 2 3 4 5 6
|
diaval |
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = { f e. T | ( R ` f ) .<_ X } ) |
8 |
7
|
eleq2d |
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( F e. ( I ` X ) <-> F e. { f e. T | ( R ` f ) .<_ X } ) ) |
9 |
|
fveq2 |
|- ( f = F -> ( R ` f ) = ( R ` F ) ) |
10 |
9
|
breq1d |
|- ( f = F -> ( ( R ` f ) .<_ X <-> ( R ` F ) .<_ X ) ) |
11 |
10
|
elrab |
|- ( F e. { f e. T | ( R ` f ) .<_ X } <-> ( F e. T /\ ( R ` F ) .<_ X ) ) |
12 |
8 11
|
syl6bb |
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( F e. ( I ` X ) <-> ( F e. T /\ ( R ` F ) .<_ X ) ) ) |