Step |
Hyp |
Ref |
Expression |
1 |
|
dibn0.b |
|- B = ( Base ` K ) |
2 |
|
dibn0.l |
|- .<_ = ( le ` K ) |
3 |
|
dibn0.h |
|- H = ( LHyp ` K ) |
4 |
|
dibn0.i |
|- I = ( ( DIsoB ` K ) ` W ) |
5 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
6 |
|
eqid |
|- ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) = ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) |
7 |
|
eqid |
|- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W ) |
8 |
1 2 3 5 6 7 4
|
dibval2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) ) |
9 |
1 2 3 7
|
dian0 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( DIsoA ` K ) ` W ) ` X ) =/= (/) ) |
10 |
|
fvex |
|- ( ( LTrn ` K ) ` W ) e. _V |
11 |
10
|
mptex |
|- ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) e. _V |
12 |
11
|
snnz |
|- { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } =/= (/) |
13 |
9 12
|
jctir |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( ( DIsoA ` K ) ` W ) ` X ) =/= (/) /\ { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } =/= (/) ) ) |
14 |
|
xpnz |
|- ( ( ( ( ( DIsoA ` K ) ` W ) ` X ) =/= (/) /\ { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } =/= (/) ) <-> ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) =/= (/) ) |
15 |
13 14
|
sylib |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { ( f e. ( ( LTrn ` K ) ` W ) |-> ( _I |` B ) ) } ) =/= (/) ) |
16 |
8 15
|
eqnetrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) =/= (/) ) |