Step |
Hyp |
Ref |
Expression |
1 |
|
llnexch.l |
|- .<_ = ( le ` K ) |
2 |
|
llnexch.j |
|- .\/ = ( join ` K ) |
3 |
|
llnexch.m |
|- ./\ = ( meet ` K ) |
4 |
|
llnexch.a |
|- A = ( Atoms ` K ) |
5 |
|
llnexch.n |
|- N = ( LLines ` K ) |
6 |
|
simpl11 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> K e. HL ) |
7 |
|
simpl21 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> P e. A ) |
8 |
|
simpl12 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> X e. N ) |
9 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
10 |
9 5
|
llnbase |
|- ( X e. N -> X e. ( Base ` K ) ) |
11 |
8 10
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> X e. ( Base ` K ) ) |
12 |
6
|
hllatd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> K e. Lat ) |
13 |
|
simpl13 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> Y e. N ) |
14 |
9 5
|
llnbase |
|- ( Y e. N -> Y e. ( Base ` K ) ) |
15 |
13 14
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> Y e. ( Base ` K ) ) |
16 |
9 3
|
latmcl |
|- ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) ) |
17 |
12 11 15 16
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) e. ( Base ` K ) ) |
18 |
9 1 3
|
latmle1 |
|- ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) .<_ X ) |
19 |
12 11 15 18
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) .<_ X ) |
20 |
9 1 2 3 4
|
atmod2i2 |
|- ( ( K e. HL /\ ( P e. A /\ X e. ( Base ` K ) /\ ( X ./\ Y ) e. ( Base ` K ) ) /\ ( X ./\ Y ) .<_ X ) -> ( ( X ./\ P ) .\/ ( X ./\ Y ) ) = ( X ./\ ( P .\/ ( X ./\ Y ) ) ) ) |
21 |
6 7 11 17 19 20
|
syl131anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( ( X ./\ P ) .\/ ( X ./\ Y ) ) = ( X ./\ ( P .\/ ( X ./\ Y ) ) ) ) |
22 |
9 4
|
atbase |
|- ( P e. A -> P e. ( Base ` K ) ) |
23 |
7 22
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> P e. ( Base ` K ) ) |
24 |
9 3
|
latmcom |
|- ( ( K e. Lat /\ X e. ( Base ` K ) /\ P e. ( Base ` K ) ) -> ( X ./\ P ) = ( P ./\ X ) ) |
25 |
12 11 23 24
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ P ) = ( P ./\ X ) ) |
26 |
|
simpl23 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> -. P .<_ X ) |
27 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
28 |
6 27
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> K e. AtLat ) |
29 |
|
eqid |
|- ( 0. ` K ) = ( 0. ` K ) |
30 |
9 1 3 29 4
|
atnle |
|- ( ( K e. AtLat /\ P e. A /\ X e. ( Base ` K ) ) -> ( -. P .<_ X <-> ( P ./\ X ) = ( 0. ` K ) ) ) |
31 |
28 7 11 30
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( -. P .<_ X <-> ( P ./\ X ) = ( 0. ` K ) ) ) |
32 |
26 31
|
mpbid |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( P ./\ X ) = ( 0. ` K ) ) |
33 |
25 32
|
eqtrd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ P ) = ( 0. ` K ) ) |
34 |
33
|
oveq1d |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( ( X ./\ P ) .\/ ( X ./\ Y ) ) = ( ( 0. ` K ) .\/ ( X ./\ Y ) ) ) |
35 |
|
simpr |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) .<_ ( P .\/ Q ) ) |
36 |
|
hlcvl |
|- ( K e. HL -> K e. CvLat ) |
37 |
6 36
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> K e. CvLat ) |
38 |
|
simpl3 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) e. A ) |
39 |
|
simpl22 |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> Q e. A ) |
40 |
|
breq1 |
|- ( P = ( X ./\ Y ) -> ( P .<_ X <-> ( X ./\ Y ) .<_ X ) ) |
41 |
19 40
|
syl5ibrcom |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( P = ( X ./\ Y ) -> P .<_ X ) ) |
42 |
41
|
necon3bd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( -. P .<_ X -> P =/= ( X ./\ Y ) ) ) |
43 |
26 42
|
mpd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> P =/= ( X ./\ Y ) ) |
44 |
43
|
necomd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) =/= P ) |
45 |
1 2 4
|
cvlatexchb1 |
|- ( ( K e. CvLat /\ ( ( X ./\ Y ) e. A /\ Q e. A /\ P e. A ) /\ ( X ./\ Y ) =/= P ) -> ( ( X ./\ Y ) .<_ ( P .\/ Q ) <-> ( P .\/ ( X ./\ Y ) ) = ( P .\/ Q ) ) ) |
46 |
37 38 39 7 44 45
|
syl131anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( ( X ./\ Y ) .<_ ( P .\/ Q ) <-> ( P .\/ ( X ./\ Y ) ) = ( P .\/ Q ) ) ) |
47 |
35 46
|
mpbid |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( P .\/ ( X ./\ Y ) ) = ( P .\/ Q ) ) |
48 |
47
|
oveq2d |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ ( P .\/ ( X ./\ Y ) ) ) = ( X ./\ ( P .\/ Q ) ) ) |
49 |
21 34 48
|
3eqtr3rd |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ ( P .\/ Q ) ) = ( ( 0. ` K ) .\/ ( X ./\ Y ) ) ) |
50 |
|
hlol |
|- ( K e. HL -> K e. OL ) |
51 |
6 50
|
syl |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> K e. OL ) |
52 |
9 2 29
|
olj02 |
|- ( ( K e. OL /\ ( X ./\ Y ) e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ ( X ./\ Y ) ) = ( X ./\ Y ) ) |
53 |
51 17 52
|
syl2anc |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( ( 0. ` K ) .\/ ( X ./\ Y ) ) = ( X ./\ Y ) ) |
54 |
49 53
|
eqtr2d |
|- ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) /\ ( X ./\ Y ) .<_ ( P .\/ Q ) ) -> ( X ./\ Y ) = ( X ./\ ( P .\/ Q ) ) ) |
55 |
54
|
ex |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( ( X ./\ Y ) .<_ ( P .\/ Q ) -> ( X ./\ Y ) = ( X ./\ ( P .\/ Q ) ) ) ) |
56 |
|
simp11 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> K e. HL ) |
57 |
56
|
hllatd |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> K e. Lat ) |
58 |
|
simp12 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> X e. N ) |
59 |
58 10
|
syl |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> X e. ( Base ` K ) ) |
60 |
|
simp21 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> P e. A ) |
61 |
|
simp22 |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> Q e. A ) |
62 |
9 2 4
|
hlatjcl |
|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) ) |
63 |
56 60 61 62
|
syl3anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( P .\/ Q ) e. ( Base ` K ) ) |
64 |
9 1 3
|
latmle2 |
|- ( ( K e. Lat /\ X e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( X ./\ ( P .\/ Q ) ) .<_ ( P .\/ Q ) ) |
65 |
57 59 63 64
|
syl3anc |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( X ./\ ( P .\/ Q ) ) .<_ ( P .\/ Q ) ) |
66 |
|
breq1 |
|- ( ( X ./\ Y ) = ( X ./\ ( P .\/ Q ) ) -> ( ( X ./\ Y ) .<_ ( P .\/ Q ) <-> ( X ./\ ( P .\/ Q ) ) .<_ ( P .\/ Q ) ) ) |
67 |
65 66
|
syl5ibrcom |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( ( X ./\ Y ) = ( X ./\ ( P .\/ Q ) ) -> ( X ./\ Y ) .<_ ( P .\/ Q ) ) ) |
68 |
55 67
|
impbid |
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( P e. A /\ Q e. A /\ -. P .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( ( X ./\ Y ) .<_ ( P .\/ Q ) <-> ( X ./\ Y ) = ( X ./\ ( P .\/ Q ) ) ) ) |