Step |
Hyp |
Ref |
Expression |
1 |
|
3dim0.j |
|- .\/ = ( join ` K ) |
2 |
|
3dim0.l |
|- .<_ = ( le ` K ) |
3 |
|
3dim0.a |
|- A = ( Atoms ` K ) |
4 |
|
eqid |
|- ( |
5 |
1 4 3
|
athgt |
|- ( K e. HL -> E. p e. A E. q e. A ( p ( |
6 |
|
df-3an |
|- ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) ) |
7 |
|
simpll1 |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> K e. HL ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
8 1 3
|
hlatjcl |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p .\/ q ) e. ( Base ` K ) ) |
10 |
9
|
ad2antrr |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( p .\/ q ) e. ( Base ` K ) ) |
11 |
|
simplr |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> r e. A ) |
12 |
8 2 1 4 3
|
cvr1 |
|- ( ( K e. HL /\ ( p .\/ q ) e. ( Base ` K ) /\ r e. A ) -> ( -. r .<_ ( p .\/ q ) <-> ( p .\/ q ) ( |
13 |
7 10 11 12
|
syl3anc |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( -. r .<_ ( p .\/ q ) <-> ( p .\/ q ) ( |
14 |
13
|
anbi2d |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) <-> ( p =/= q /\ ( p .\/ q ) ( |
15 |
7
|
hllatd |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> K e. Lat ) |
16 |
8 3
|
atbase |
|- ( r e. A -> r e. ( Base ` K ) ) |
17 |
16
|
ad2antlr |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> r e. ( Base ` K ) ) |
18 |
8 1
|
latjcl |
|- ( ( K e. Lat /\ ( p .\/ q ) e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) ) |
19 |
15 10 17 18
|
syl3anc |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) ) |
20 |
|
simpr |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> s e. A ) |
21 |
8 2 1 4 3
|
cvr1 |
|- ( ( K e. HL /\ ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) /\ s e. A ) -> ( -. s .<_ ( ( p .\/ q ) .\/ r ) <-> ( ( p .\/ q ) .\/ r ) ( |
22 |
7 19 20 21
|
syl3anc |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( -. s .<_ ( ( p .\/ q ) .\/ r ) <-> ( ( p .\/ q ) .\/ r ) ( |
23 |
14 22
|
anbi12d |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( ( p =/= q /\ ( p .\/ q ) ( |
24 |
6 23
|
syl5bb |
|- ( ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) /\ s e. A ) -> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( ( p =/= q /\ ( p .\/ q ) ( |
25 |
24
|
rexbidva |
|- ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) -> ( E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> E. s e. A ( ( p =/= q /\ ( p .\/ q ) ( |
26 |
|
r19.42v |
|- ( E. s e. A ( ( p =/= q /\ ( p .\/ q ) ( ( ( p =/= q /\ ( p .\/ q ) ( |
27 |
|
anass |
|- ( ( ( p =/= q /\ ( p .\/ q ) ( ( p =/= q /\ ( ( p .\/ q ) ( |
28 |
26 27
|
bitri |
|- ( E. s e. A ( ( p =/= q /\ ( p .\/ q ) ( ( p =/= q /\ ( ( p .\/ q ) ( |
29 |
25 28
|
syl6bb |
|- ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ r e. A ) -> ( E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p =/= q /\ ( ( p .\/ q ) ( |
30 |
29
|
rexbidva |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> E. r e. A ( p =/= q /\ ( ( p .\/ q ) ( |
31 |
|
r19.42v |
|- ( E. r e. A ( p =/= q /\ ( ( p .\/ q ) ( ( p =/= q /\ E. r e. A ( ( p .\/ q ) ( |
32 |
30 31
|
syl6bb |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p =/= q /\ E. r e. A ( ( p .\/ q ) ( |
33 |
1 4 3
|
atcvr1 |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p =/= q <-> p ( |
34 |
33
|
anbi1d |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( ( p =/= q /\ E. r e. A ( ( p .\/ q ) ( ( p ( |
35 |
32 34
|
bitrd |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p ( |
36 |
35
|
3expb |
|- ( ( K e. HL /\ ( p e. A /\ q e. A ) ) -> ( E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p ( |
37 |
36
|
2rexbidva |
|- ( K e. HL -> ( E. p e. A E. q e. A E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> E. p e. A E. q e. A ( p ( |
38 |
5 37
|
mpbird |
|- ( K e. HL -> E. p e. A E. q e. A E. r e. A E. s e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) ) |