Step |
Hyp |
Ref |
Expression |
1 |
|
atomle.b |
|- B = ( Base ` K ) |
2 |
|
atomle.l |
|- .<_ = ( le ` K ) |
3 |
|
atomle.j |
|- .\/ = ( join ` K ) |
4 |
|
atomle.a |
|- A = ( Atoms ` K ) |
5 |
|
simpl32 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> -. Q .<_ X ) |
6 |
|
simp11l |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> K e. HL ) |
7 |
6
|
hllatd |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> K e. Lat ) |
8 |
|
simp122 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q e. A ) |
9 |
1 4
|
atbase |
|- ( Q e. A -> Q e. B ) |
10 |
8 9
|
syl |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q e. B ) |
11 |
|
simp121 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P e. A ) |
12 |
1 4
|
atbase |
|- ( P e. A -> P e. B ) |
13 |
11 12
|
syl |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P e. B ) |
14 |
|
simp123 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R e. A ) |
15 |
1 4
|
atbase |
|- ( R e. A -> R e. B ) |
16 |
14 15
|
syl |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R e. B ) |
17 |
1 3
|
latjcl |
|- ( ( K e. Lat /\ P e. B /\ R e. B ) -> ( P .\/ R ) e. B ) |
18 |
7 13 16 17
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( P .\/ R ) e. B ) |
19 |
|
simp11r |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> X e. B ) |
20 |
14 8 11
|
3jca |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( R e. A /\ Q e. A /\ P e. A ) ) |
21 |
|
simp2 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R =/= P ) |
22 |
6 20 21
|
3jca |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) ) |
23 |
|
simp133 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R .<_ ( P .\/ Q ) ) |
24 |
2 3 4
|
hlatexch1 |
|- ( ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) -> ( R .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ R ) ) ) |
25 |
22 23 24
|
sylc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q .<_ ( P .\/ R ) ) |
26 |
|
simp131 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P .<_ X ) |
27 |
|
simp3 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R .<_ X ) |
28 |
1 2 3
|
latjle12 |
|- ( ( K e. Lat /\ ( P e. B /\ R e. B /\ X e. B ) ) -> ( ( P .<_ X /\ R .<_ X ) <-> ( P .\/ R ) .<_ X ) ) |
29 |
7 13 16 19 28
|
syl13anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( ( P .<_ X /\ R .<_ X ) <-> ( P .\/ R ) .<_ X ) ) |
30 |
26 27 29
|
mpbi2and |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( P .\/ R ) .<_ X ) |
31 |
1 2 7 10 18 19 25 30
|
lattrd |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q .<_ X ) |
32 |
31
|
3expia |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> ( R .<_ X -> Q .<_ X ) ) |
33 |
5 32
|
mtod |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> -. R .<_ X ) |
34 |
33
|
ex |
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R =/= P -> -. R .<_ X ) ) |
35 |
34
|
necon4ad |
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X -> R = P ) ) |
36 |
|
simp31 |
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> P .<_ X ) |
37 |
|
breq1 |
|- ( R = P -> ( R .<_ X <-> P .<_ X ) ) |
38 |
36 37
|
syl5ibrcom |
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R = P -> R .<_ X ) ) |
39 |
35 38
|
impbid |
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X <-> R = P ) ) |