Step |
Hyp |
Ref |
Expression |
1 |
|
djacl.h |
|- H = ( LHyp ` K ) |
2 |
|
djacl.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
djacl.i |
|- I = ( ( DIsoA ` K ) ` W ) |
4 |
|
djacl.j |
|- J = ( ( vA ` K ) ` W ) |
5 |
|
eqid |
|- ( ( ocA ` K ) ` W ) = ( ( ocA ` K ) ` W ) |
6 |
1 2 3 5 4
|
djavalN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) = ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) ) |
7 |
|
inss1 |
|- ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ ( ( ( ocA ` K ) ` W ) ` X ) |
8 |
1 2 3 5
|
docaclN |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ T ) -> ( ( ( ocA ` K ) ` W ) ` X ) e. ran I ) |
9 |
8
|
adantrr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` X ) e. ran I ) |
10 |
1 2 3
|
diaelrnN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ocA ` K ) ` W ) ` X ) e. ran I ) -> ( ( ( ocA ` K ) ` W ) ` X ) C_ T ) |
11 |
9 10
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` X ) C_ T ) |
12 |
7 11
|
sstrid |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ T ) |
13 |
1 2 3 5
|
docaclN |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) C_ T ) -> ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) e. ran I ) |
14 |
12 13
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( ( ( ocA ` K ) ` W ) ` ( ( ( ( ocA ` K ) ` W ) ` X ) i^i ( ( ( ocA ` K ) ` W ) ` Y ) ) ) e. ran I ) |
15 |
6 14
|
eqeltrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ T /\ Y C_ T ) ) -> ( X J Y ) e. ran I ) |