Step |
Hyp |
Ref |
Expression |
1 |
|
dihjatc.b |
|- B = ( Base ` K ) |
2 |
|
dihjatc.l |
|- .<_ = ( le ` K ) |
3 |
|
dihjatc.h |
|- H = ( LHyp ` K ) |
4 |
|
dihjatc.j |
|- .\/ = ( join ` K ) |
5 |
|
dihjatc.a |
|- A = ( Atoms ` K ) |
6 |
|
dihjatc.u |
|- U = ( ( DVecH ` K ) ` W ) |
7 |
|
dihjatc.s |
|- .(+) = ( LSSum ` U ) |
8 |
|
dihjatc.i |
|- I = ( ( DIsoH ` K ) ` W ) |
9 |
|
dihjatc.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
10 |
|
dihjatc.x |
|- ( ph -> ( X e. B /\ X .<_ W ) ) |
11 |
|
dihjatc.p |
|- ( ph -> ( P e. A /\ -. P .<_ W ) ) |
12 |
9
|
simpld |
|- ( ph -> K e. HL ) |
13 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
14 |
12 13
|
syl |
|- ( ph -> K e. OP ) |
15 |
|
eqid |
|- ( 1. ` K ) = ( 1. ` K ) |
16 |
1 15
|
op1cl |
|- ( K e. OP -> ( 1. ` K ) e. B ) |
17 |
14 16
|
syl |
|- ( ph -> ( 1. ` K ) e. B ) |
18 |
10
|
simpld |
|- ( ph -> X e. B ) |
19 |
11
|
simpld |
|- ( ph -> P e. A ) |
20 |
1 5
|
atbase |
|- ( P e. A -> P e. B ) |
21 |
19 20
|
syl |
|- ( ph -> P e. B ) |
22 |
1 2 15
|
ople1 |
|- ( ( K e. OP /\ P e. B ) -> P .<_ ( 1. ` K ) ) |
23 |
14 21 22
|
syl2anc |
|- ( ph -> P .<_ ( 1. ` K ) ) |
24 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
25 |
12 24
|
syl |
|- ( ph -> K e. OL ) |
26 |
|
eqid |
|- ( meet ` K ) = ( meet ` K ) |
27 |
1 26 15
|
olm12 |
|- ( ( K e. OL /\ X e. B ) -> ( ( 1. ` K ) ( meet ` K ) X ) = X ) |
28 |
25 18 27
|
syl2anc |
|- ( ph -> ( ( 1. ` K ) ( meet ` K ) X ) = X ) |
29 |
10
|
simprd |
|- ( ph -> X .<_ W ) |
30 |
28 29
|
eqbrtrd |
|- ( ph -> ( ( 1. ` K ) ( meet ` K ) X ) .<_ W ) |
31 |
1 2 3 4 26 5 6 7 8
|
dihjatc3 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( 1. ` K ) e. B /\ X e. B ) /\ ( P e. A /\ -. P .<_ W ) /\ ( P .<_ ( 1. ` K ) /\ ( ( 1. ` K ) ( meet ` K ) X ) .<_ W ) ) -> ( I ` ( ( ( 1. ` K ) ( meet ` K ) X ) .\/ P ) ) = ( ( I ` ( ( 1. ` K ) ( meet ` K ) X ) ) .(+) ( I ` P ) ) ) |
32 |
9 17 18 11 23 30 31
|
syl312anc |
|- ( ph -> ( I ` ( ( ( 1. ` K ) ( meet ` K ) X ) .\/ P ) ) = ( ( I ` ( ( 1. ` K ) ( meet ` K ) X ) ) .(+) ( I ` P ) ) ) |
33 |
28
|
fvoveq1d |
|- ( ph -> ( I ` ( ( ( 1. ` K ) ( meet ` K ) X ) .\/ P ) ) = ( I ` ( X .\/ P ) ) ) |
34 |
28
|
fveq2d |
|- ( ph -> ( I ` ( ( 1. ` K ) ( meet ` K ) X ) ) = ( I ` X ) ) |
35 |
34
|
oveq1d |
|- ( ph -> ( ( I ` ( ( 1. ` K ) ( meet ` K ) X ) ) .(+) ( I ` P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) ) |
36 |
32 33 35
|
3eqtr3d |
|- ( ph -> ( I ` ( X .\/ P ) ) = ( ( I ` X ) .(+) ( I ` P ) ) ) |