Step |
Hyp |
Ref |
Expression |
1 |
|
dochoc.h |
|- H = ( LHyp ` K ) |
2 |
|
dochoc.i |
|- I = ( ( DIsoH ` K ) ` W ) |
3 |
|
dochoc.o |
|- ._|_ = ( ( ocH ` K ) ` W ) |
4 |
|
eqid |
|- ( oc ` K ) = ( oc ` K ) |
5 |
4 1 2 3
|
dochvalr |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` X ) = ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) |
6 |
5
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) |
7 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
8 |
7
|
ad2antrr |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> K e. OP ) |
9 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
10 |
9 1 2
|
dihcnvcl |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) ) |
11 |
9 4
|
opoccl |
|- ( ( K e. OP /\ ( `' I ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( `' I ` X ) ) e. ( Base ` K ) ) |
12 |
8 10 11
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( oc ` K ) ` ( `' I ` X ) ) e. ( Base ` K ) ) |
13 |
9 1 2
|
dihcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( oc ` K ) ` ( `' I ` X ) ) e. ( Base ` K ) ) -> ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) e. ran I ) |
14 |
12 13
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) e. ran I ) |
15 |
4 1 2 3
|
dochvalr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) e. ran I ) -> ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) = ( I ` ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) ) ) |
16 |
14 15
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) = ( I ` ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) ) ) |
17 |
9 1 2
|
dihcnvid1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( oc ` K ) ` ( `' I ` X ) ) e. ( Base ` K ) ) -> ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) = ( ( oc ` K ) ` ( `' I ` X ) ) ) |
18 |
12 17
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) = ( ( oc ` K ) ` ( `' I ` X ) ) ) |
19 |
18
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) = ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) |
20 |
9 4
|
opococ |
|- ( ( K e. OP /\ ( `' I ` X ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` X ) ) ) = ( `' I ` X ) ) |
21 |
8 10 20
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` ( `' I ` X ) ) ) = ( `' I ` X ) ) |
22 |
19 21
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) = ( `' I ` X ) ) |
23 |
22
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) ) = ( I ` ( `' I ` X ) ) ) |
24 |
1 2
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X ) |
25 |
23 24
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( ( oc ` K ) ` ( `' I ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) ) ) = X ) |
26 |
16 25
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( I ` ( ( oc ` K ) ` ( `' I ` X ) ) ) ) = X ) |
27 |
6 26
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ._|_ ` X ) ) = X ) |