| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dihjat4.j |
|- .\/ = ( join ` K ) |
| 2 |
|
dihjat4.h |
|- H = ( LHyp ` K ) |
| 3 |
|
dihjat4.i |
|- I = ( ( DIsoH ` K ) ` W ) |
| 4 |
|
dihjat4.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 5 |
|
dihjat4.s |
|- .(+) = ( LSSum ` U ) |
| 6 |
|
dihjat4.a |
|- A = ( LSAtoms ` U ) |
| 7 |
|
dihjat4.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 8 |
|
dihjat4.x |
|- ( ph -> X e. ran I ) |
| 9 |
|
dihjat4.q |
|- ( ph -> Q e. A ) |
| 10 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
| 11 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
| 12 |
10 2 3
|
dihcnvcl |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) ) |
| 13 |
7 8 12
|
syl2anc |
|- ( ph -> ( `' I ` X ) e. ( Base ` K ) ) |
| 14 |
11 2 4 3 6
|
dihlatat |
|- ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> ( `' I ` Q ) e. ( Atoms ` K ) ) |
| 15 |
7 9 14
|
syl2anc |
|- ( ph -> ( `' I ` Q ) e. ( Atoms ` K ) ) |
| 16 |
10 2 1 11 4 5 3 7 13 15
|
dihjat3 |
|- ( ph -> ( I ` ( ( `' I ` X ) .\/ ( `' I ` Q ) ) ) = ( ( I ` ( `' I ` X ) ) .(+) ( I ` ( `' I ` Q ) ) ) ) |
| 17 |
2 3
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X ) |
| 18 |
7 8 17
|
syl2anc |
|- ( ph -> ( I ` ( `' I ` X ) ) = X ) |
| 19 |
2 4 3 6
|
dih1dimat |
|- ( ( ( K e. HL /\ W e. H ) /\ Q e. A ) -> Q e. ran I ) |
| 20 |
7 9 19
|
syl2anc |
|- ( ph -> Q e. ran I ) |
| 21 |
2 3
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ Q e. ran I ) -> ( I ` ( `' I ` Q ) ) = Q ) |
| 22 |
7 20 21
|
syl2anc |
|- ( ph -> ( I ` ( `' I ` Q ) ) = Q ) |
| 23 |
18 22
|
oveq12d |
|- ( ph -> ( ( I ` ( `' I ` X ) ) .(+) ( I ` ( `' I ` Q ) ) ) = ( X .(+) Q ) ) |
| 24 |
16 23
|
eqtr2d |
|- ( ph -> ( X .(+) Q ) = ( I ` ( ( `' I ` X ) .\/ ( `' I ` Q ) ) ) ) |