Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme8.l |
|- .<_ = ( le ` K ) |
2 |
|
cdleme8.j |
|- .\/ = ( join ` K ) |
3 |
|
cdleme8.m |
|- ./\ = ( meet ` K ) |
4 |
|
cdleme8.a |
|- A = ( Atoms ` K ) |
5 |
|
cdleme8.h |
|- H = ( LHyp ` K ) |
6 |
|
cdleme8.4 |
|- C = ( ( P .\/ S ) ./\ W ) |
7 |
6
|
oveq2i |
|- ( P .\/ C ) = ( P .\/ ( ( P .\/ S ) ./\ W ) ) |
8 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> K e. HL ) |
9 |
|
simp2l |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> P e. A ) |
10 |
8
|
hllatd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> K e. Lat ) |
11 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
12 |
11 4
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
13 |
9 12
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> P e. ( Base ` K ) ) |
14 |
11 4
|
atbase |
|- ( S e. A -> S e. ( Base ` K ) ) |
15 |
14
|
3ad2ant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> S e. ( Base ` K ) ) |
16 |
11 2
|
latjcl |
|- ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( P .\/ S ) e. ( Base ` K ) ) |
17 |
10 13 15 16
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( P .\/ S ) e. ( Base ` K ) ) |
18 |
|
simp1r |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> W e. H ) |
19 |
11 5
|
lhpbase |
|- ( W e. H -> W e. ( Base ` K ) ) |
20 |
18 19
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> W e. ( Base ` K ) ) |
21 |
11 1 2
|
latlej1 |
|- ( ( K e. Lat /\ P e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> P .<_ ( P .\/ S ) ) |
22 |
10 13 15 21
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> P .<_ ( P .\/ S ) ) |
23 |
11 1 2 3 4
|
atmod3i1 |
|- ( ( K e. HL /\ ( P e. A /\ ( P .\/ S ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) /\ P .<_ ( P .\/ S ) ) -> ( P .\/ ( ( P .\/ S ) ./\ W ) ) = ( ( P .\/ S ) ./\ ( P .\/ W ) ) ) |
24 |
8 9 17 20 22 23
|
syl131anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( P .\/ ( ( P .\/ S ) ./\ W ) ) = ( ( P .\/ S ) ./\ ( P .\/ W ) ) ) |
25 |
|
eqid |
|- ( 1. ` K ) = ( 1. ` K ) |
26 |
1 2 25 4 5
|
lhpjat2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = ( 1. ` K ) ) |
27 |
26
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( P .\/ W ) = ( 1. ` K ) ) |
28 |
27
|
oveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( ( P .\/ S ) ./\ ( P .\/ W ) ) = ( ( P .\/ S ) ./\ ( 1. ` K ) ) ) |
29 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
30 |
8 29
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> K e. OL ) |
31 |
11 3 25
|
olm11 |
|- ( ( K e. OL /\ ( P .\/ S ) e. ( Base ` K ) ) -> ( ( P .\/ S ) ./\ ( 1. ` K ) ) = ( P .\/ S ) ) |
32 |
30 17 31
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( ( P .\/ S ) ./\ ( 1. ` K ) ) = ( P .\/ S ) ) |
33 |
24 28 32
|
3eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( P .\/ ( ( P .\/ S ) ./\ W ) ) = ( P .\/ S ) ) |
34 |
7 33
|
syl5eq |
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ S e. A ) -> ( P .\/ C ) = ( P .\/ S ) ) |