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