Step |
Hyp |
Ref |
Expression |
1 |
|
islln3.b |
|- B = ( Base ` K ) |
2 |
|
islln3.j |
|- .\/ = ( join ` K ) |
3 |
|
islln3.a |
|- A = ( Atoms ` K ) |
4 |
|
islln3.n |
|- N = ( LLines ` K ) |
5 |
|
eqid |
|- ( |
6 |
1 5 3 4
|
islln4 |
|- ( ( K e. HL /\ X e. B ) -> ( X e. N <-> E. p e. A p ( |
7 |
|
simpll |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> K e. HL ) |
8 |
1 3
|
atbase |
|- ( p e. A -> p e. B ) |
9 |
8
|
adantl |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> p e. B ) |
10 |
|
simplr |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> X e. B ) |
11 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
12 |
1 11 2 5 3
|
cvrval3 |
|- ( ( K e. HL /\ p e. B /\ X e. B ) -> ( p ( E. q e. A ( -. q ( le ` K ) p /\ ( p .\/ q ) = X ) ) ) |
13 |
7 9 10 12
|
syl3anc |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> ( p ( E. q e. A ( -. q ( le ` K ) p /\ ( p .\/ q ) = X ) ) ) |
14 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
15 |
14
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> K e. AtLat ) |
16 |
|
simpr |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> q e. A ) |
17 |
|
simplr |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> p e. A ) |
18 |
11 3
|
atncmp |
|- ( ( K e. AtLat /\ q e. A /\ p e. A ) -> ( -. q ( le ` K ) p <-> q =/= p ) ) |
19 |
15 16 17 18
|
syl3anc |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> ( -. q ( le ` K ) p <-> q =/= p ) ) |
20 |
|
necom |
|- ( q =/= p <-> p =/= q ) |
21 |
19 20
|
bitrdi |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> ( -. q ( le ` K ) p <-> p =/= q ) ) |
22 |
|
eqcom |
|- ( ( p .\/ q ) = X <-> X = ( p .\/ q ) ) |
23 |
22
|
a1i |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> ( ( p .\/ q ) = X <-> X = ( p .\/ q ) ) ) |
24 |
21 23
|
anbi12d |
|- ( ( ( ( K e. HL /\ X e. B ) /\ p e. A ) /\ q e. A ) -> ( ( -. q ( le ` K ) p /\ ( p .\/ q ) = X ) <-> ( p =/= q /\ X = ( p .\/ q ) ) ) ) |
25 |
24
|
rexbidva |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> ( E. q e. A ( -. q ( le ` K ) p /\ ( p .\/ q ) = X ) <-> E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) |
26 |
13 25
|
bitrd |
|- ( ( ( K e. HL /\ X e. B ) /\ p e. A ) -> ( p ( E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) |
27 |
26
|
rexbidva |
|- ( ( K e. HL /\ X e. B ) -> ( E. p e. A p ( E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) |
28 |
6 27
|
bitrd |
|- ( ( K e. HL /\ X e. B ) -> ( X e. N <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) ) |