Metamath Proof Explorer


Theorem islln3

Description: The predicate "is a lattice line". (Contributed by NM, 17-Jun-2012)

Ref Expression
Hypotheses islln3.b
|- B = ( Base ` K )
islln3.j
|- .\/ = ( join ` K )
islln3.a
|- A = ( Atoms ` K )
islln3.n
|- N = ( LLines ` K )
Assertion islln3
|- ( ( K e. HL /\ X e. B ) -> ( X e. N <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) )

Proof

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 ) ) ) )