Step |
Hyp |
Ref |
Expression |
1 |
|
djhj.k |
|- .\/ = ( join ` K ) |
2 |
|
djhj.h |
|- H = ( LHyp ` K ) |
3 |
|
djhj.i |
|- I = ( ( DIsoH ` K ) ` W ) |
4 |
|
djhj.j |
|- J = ( ( joinH ` K ) ` W ) |
5 |
|
djhj.w |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
6 |
|
djhj.x |
|- ( ph -> X e. ran I ) |
7 |
|
djhj.y |
|- ( ph -> Y e. ran I ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
8 2 3
|
dihcnvcl |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) ) |
10 |
5 6 9
|
syl2anc |
|- ( ph -> ( `' I ` X ) e. ( Base ` K ) ) |
11 |
8 2 3
|
dihcnvcl |
|- ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( `' I ` Y ) e. ( Base ` K ) ) |
12 |
5 7 11
|
syl2anc |
|- ( ph -> ( `' I ` Y ) e. ( Base ` K ) ) |
13 |
8 1 2 3 4
|
djhlj |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( `' I ` X ) e. ( Base ` K ) /\ ( `' I ` Y ) e. ( Base ` K ) ) ) -> ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) = ( ( I ` ( `' I ` X ) ) J ( I ` ( `' I ` Y ) ) ) ) |
14 |
5 10 12 13
|
syl12anc |
|- ( ph -> ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) = ( ( I ` ( `' I ` X ) ) J ( I ` ( `' I ` Y ) ) ) ) |
15 |
2 3
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X ) |
16 |
5 6 15
|
syl2anc |
|- ( ph -> ( I ` ( `' I ` X ) ) = X ) |
17 |
2 3
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ Y e. ran I ) -> ( I ` ( `' I ` Y ) ) = Y ) |
18 |
5 7 17
|
syl2anc |
|- ( ph -> ( I ` ( `' I ` Y ) ) = Y ) |
19 |
16 18
|
oveq12d |
|- ( ph -> ( ( I ` ( `' I ` X ) ) J ( I ` ( `' I ` Y ) ) ) = ( X J Y ) ) |
20 |
14 19
|
eqtr2d |
|- ( ph -> ( X J Y ) = ( I ` ( ( `' I ` X ) .\/ ( `' I ` Y ) ) ) ) |