Step |
Hyp |
Ref |
Expression |
1 |
|
llnle.b |
|- B = ( Base ` K ) |
2 |
|
llnle.l |
|- .<_ = ( le ` K ) |
3 |
|
llnle.z |
|- .0. = ( 0. ` K ) |
4 |
|
llnle.a |
|- A = ( Atoms ` K ) |
5 |
|
llnle.n |
|- N = ( LLines ` K ) |
6 |
|
simpll |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> K e. HL ) |
7 |
|
simplr |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> X e. B ) |
8 |
|
simprl |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> X =/= .0. ) |
9 |
1 2 3 4
|
atle |
|- ( ( K e. HL /\ X e. B /\ X =/= .0. ) -> E. p e. A p .<_ X ) |
10 |
6 7 8 9
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> E. p e. A p .<_ X ) |
11 |
|
simp1ll |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> K e. HL ) |
12 |
1 4
|
atbase |
|- ( p e. A -> p e. B ) |
13 |
12
|
3ad2ant2 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p e. B ) |
14 |
|
simp1lr |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> X e. B ) |
15 |
|
simp3 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p .<_ X ) |
16 |
|
simp2 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p e. A ) |
17 |
|
simp1rr |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> -. X e. A ) |
18 |
|
nelne2 |
|- ( ( p e. A /\ -. X e. A ) -> p =/= X ) |
19 |
16 17 18
|
syl2anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p =/= X ) |
20 |
|
eqid |
|- ( lt ` K ) = ( lt ` K ) |
21 |
2 20
|
pltval |
|- ( ( K e. HL /\ p e. A /\ X e. B ) -> ( p ( lt ` K ) X <-> ( p .<_ X /\ p =/= X ) ) ) |
22 |
11 16 14 21
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( p ( lt ` K ) X <-> ( p .<_ X /\ p =/= X ) ) ) |
23 |
15 19 22
|
mpbir2and |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> p ( lt ` K ) X ) |
24 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
25 |
|
eqid |
|- ( |
26 |
1 2 20 24 25 4
|
hlrelat3 |
|- ( ( ( K e. HL /\ p e. B /\ X e. B ) /\ p ( lt ` K ) X ) -> E. q e. A ( p ( |
27 |
11 13 14 23 26
|
syl31anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> E. q e. A ( p ( |
28 |
|
simp1ll |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( K e. HL ) |
29 |
|
simp21 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( p e. A ) |
30 |
|
simp23 |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( q e. A ) |
31 |
1 24 4
|
hlatjcl |
|- ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p ( join ` K ) q ) e. B ) |
32 |
28 29 30 31
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( ( p ( join ` K ) q ) e. B ) |
33 |
|
simp3l |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( p ( |
34 |
1 25 4 5
|
llni |
|- ( ( ( K e. HL /\ ( p ( join ` K ) q ) e. B /\ p e. A ) /\ p ( ( p ( join ` K ) q ) e. N ) |
35 |
28 32 29 33 34
|
syl31anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( ( p ( join ` K ) q ) e. N ) |
36 |
|
simp3r |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( ( p ( join ` K ) q ) .<_ X ) |
37 |
|
breq1 |
|- ( y = ( p ( join ` K ) q ) -> ( y .<_ X <-> ( p ( join ` K ) q ) .<_ X ) ) |
38 |
37
|
rspcev |
|- ( ( ( p ( join ` K ) q ) e. N /\ ( p ( join ` K ) q ) .<_ X ) -> E. y e. N y .<_ X ) |
39 |
35 36 38
|
syl2anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ ( p e. A /\ p .<_ X /\ q e. A ) /\ ( p ( E. y e. N y .<_ X ) |
40 |
39
|
3exp |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( ( p e. A /\ p .<_ X /\ q e. A ) -> ( ( p ( E. y e. N y .<_ X ) ) ) |
41 |
40
|
3expd |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( p e. A -> ( p .<_ X -> ( q e. A -> ( ( p ( E. y e. N y .<_ X ) ) ) ) ) |
42 |
41
|
3imp |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( q e. A -> ( ( p ( E. y e. N y .<_ X ) ) ) |
43 |
42
|
rexlimdv |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> ( E. q e. A ( p ( E. y e. N y .<_ X ) ) |
44 |
27 43
|
mpd |
|- ( ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) /\ p e. A /\ p .<_ X ) -> E. y e. N y .<_ X ) |
45 |
44
|
3exp |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( p e. A -> ( p .<_ X -> E. y e. N y .<_ X ) ) ) |
46 |
45
|
rexlimdv |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> ( E. p e. A p .<_ X -> E. y e. N y .<_ X ) ) |
47 |
10 46
|
mpd |
|- ( ( ( K e. HL /\ X e. B ) /\ ( X =/= .0. /\ -. X e. A ) ) -> E. y e. N y .<_ X ) |