Step |
Hyp |
Ref |
Expression |
1 |
|
lncmp.b |
|- B = ( Base ` K ) |
2 |
|
lncmp.l |
|- .<_ = ( le ` K ) |
3 |
|
lncmp.n |
|- N = ( Lines ` K ) |
4 |
|
lncmp.m |
|- M = ( pmap ` K ) |
5 |
|
simplrl |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( M ` X ) e. N ) |
6 |
|
simpll1 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> K e. HL ) |
7 |
|
simpll2 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> X e. B ) |
8 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
9 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
10 |
1 8 9 3 4
|
isline3 |
|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) |
11 |
6 7 10
|
syl2anc |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( M ` X ) e. N <-> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) |
12 |
5 11
|
mpbid |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) |
13 |
|
simp3rr |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X = ( p ( join ` K ) q ) ) |
14 |
|
simp1l1 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> K e. HL ) |
15 |
|
simp1l3 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> Y e. B ) |
16 |
|
simp1rr |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> ( M ` Y ) e. N ) |
17 |
|
simp3ll |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p e. ( Atoms ` K ) ) |
18 |
|
simp3lr |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q e. ( Atoms ` K ) ) |
19 |
|
simp3rl |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p =/= q ) |
20 |
14
|
hllatd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> K e. Lat ) |
21 |
1 9
|
atbase |
|- ( p e. ( Atoms ` K ) -> p e. B ) |
22 |
17 21
|
syl |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p e. B ) |
23 |
|
simp1l2 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X e. B ) |
24 |
2 8 9
|
hlatlej1 |
|- ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> p .<_ ( p ( join ` K ) q ) ) |
25 |
14 17 18 24
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ ( p ( join ` K ) q ) ) |
26 |
25 13
|
breqtrrd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ X ) |
27 |
|
simp2 |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X .<_ Y ) |
28 |
1 2 20 22 23 15 26 27
|
lattrd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> p .<_ Y ) |
29 |
1 9
|
atbase |
|- ( q e. ( Atoms ` K ) -> q e. B ) |
30 |
18 29
|
syl |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q e. B ) |
31 |
2 8 9
|
hlatlej2 |
|- ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> q .<_ ( p ( join ` K ) q ) ) |
32 |
14 17 18 31
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ ( p ( join ` K ) q ) ) |
33 |
32 13
|
breqtrrd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ X ) |
34 |
1 2 20 30 23 15 33 27
|
lattrd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> q .<_ Y ) |
35 |
1 2 8 9 3 4
|
lneq2at |
|- ( ( ( K e. HL /\ Y e. B /\ ( M ` Y ) e. N ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) /\ p =/= q ) /\ ( p .<_ Y /\ q .<_ Y ) ) -> Y = ( p ( join ` K ) q ) ) |
36 |
14 15 16 17 18 19 28 34 35
|
syl332anc |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> Y = ( p ( join ` K ) q ) ) |
37 |
13 36
|
eqtr4d |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y /\ ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) -> X = Y ) |
38 |
37
|
3expia |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) -> X = Y ) ) |
39 |
38
|
expd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> X = Y ) ) ) |
40 |
39
|
rexlimdvv |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> ( E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> X = Y ) ) |
41 |
12 40
|
mpd |
|- ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) /\ X .<_ Y ) -> X = Y ) |
42 |
41
|
ex |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X .<_ Y -> X = Y ) ) |
43 |
|
simpl1 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> K e. HL ) |
44 |
43
|
hllatd |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> K e. Lat ) |
45 |
|
simpl2 |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> X e. B ) |
46 |
1 2
|
latref |
|- ( ( K e. Lat /\ X e. B ) -> X .<_ X ) |
47 |
44 45 46
|
syl2anc |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> X .<_ X ) |
48 |
|
breq2 |
|- ( X = Y -> ( X .<_ X <-> X .<_ Y ) ) |
49 |
47 48
|
syl5ibcom |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X = Y -> X .<_ Y ) ) |
50 |
42 49
|
impbid |
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( M ` X ) e. N /\ ( M ` Y ) e. N ) ) -> ( X .<_ Y <-> X = Y ) ) |