Metamath Proof Explorer


Theorem llnexatN

Description: Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses llnexat.l
|- .<_ = ( le ` K )
llnexat.j
|- .\/ = ( join ` K )
llnexat.a
|- A = ( Atoms ` K )
llnexat.n
|- N = ( LLines ` K )
Assertion llnexatN
|- ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> E. q e. A ( P =/= q /\ X = ( P .\/ q ) ) )

Proof

Step Hyp Ref Expression
1 llnexat.l
 |-  .<_ = ( le ` K )
2 llnexat.j
 |-  .\/ = ( join ` K )
3 llnexat.a
 |-  A = ( Atoms ` K )
4 llnexat.n
 |-  N = ( LLines ` K )
5 simp1
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> K e. HL )
6 simp3
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> P e. A )
7 simp2
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> X e. N )
8 5 6 7 3jca
 |-  ( ( K e. HL /\ X e. N /\ P e. A ) -> ( K e. HL /\ P e. A /\ X e. N ) )
9 eqid
 |-  ( 
10 1 9 3 4 atcvrlln2
 |-  ( ( ( K e. HL /\ P e. A /\ X e. N ) /\ P .<_ X ) -> P ( 
11 8 10 sylan
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> P ( 
12 simpl1
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> K e. HL )
13 simpl3
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> P e. A )
14 eqid
 |-  ( Base ` K ) = ( Base ` K )
15 14 3 atbase
 |-  ( P e. A -> P e. ( Base ` K ) )
16 13 15 syl
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> P e. ( Base ` K ) )
17 simpl2
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> X e. N )
18 14 4 llnbase
 |-  ( X e. N -> X e. ( Base ` K ) )
19 17 18 syl
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> X e. ( Base ` K ) )
20 14 1 2 9 3 cvrval3
 |-  ( ( K e. HL /\ P e. ( Base ` K ) /\ X e. ( Base ` K ) ) -> ( P (  E. q e. A ( -. q .<_ P /\ ( P .\/ q ) = X ) ) )
21 12 16 19 20 syl3anc
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> ( P (  E. q e. A ( -. q .<_ P /\ ( P .\/ q ) = X ) ) )
22 simpll1
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> K e. HL )
23 hlatl
 |-  ( K e. HL -> K e. AtLat )
24 22 23 syl
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> K e. AtLat )
25 simpr
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> q e. A )
26 simpll3
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> P e. A )
27 1 3 atncmp
 |-  ( ( K e. AtLat /\ q e. A /\ P e. A ) -> ( -. q .<_ P <-> q =/= P ) )
28 24 25 26 27 syl3anc
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> ( -. q .<_ P <-> q =/= P ) )
29 28 anbi1d
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> ( ( -. q .<_ P /\ ( P .\/ q ) = X ) <-> ( q =/= P /\ ( P .\/ q ) = X ) ) )
30 necom
 |-  ( q =/= P <-> P =/= q )
31 eqcom
 |-  ( ( P .\/ q ) = X <-> X = ( P .\/ q ) )
32 30 31 anbi12i
 |-  ( ( q =/= P /\ ( P .\/ q ) = X ) <-> ( P =/= q /\ X = ( P .\/ q ) ) )
33 29 32 bitrdi
 |-  ( ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) /\ q e. A ) -> ( ( -. q .<_ P /\ ( P .\/ q ) = X ) <-> ( P =/= q /\ X = ( P .\/ q ) ) ) )
34 33 rexbidva
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> ( E. q e. A ( -. q .<_ P /\ ( P .\/ q ) = X ) <-> E. q e. A ( P =/= q /\ X = ( P .\/ q ) ) ) )
35 21 34 bitrd
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> ( P (  E. q e. A ( P =/= q /\ X = ( P .\/ q ) ) ) )
36 11 35 mpbid
 |-  ( ( ( K e. HL /\ X e. N /\ P e. A ) /\ P .<_ X ) -> E. q e. A ( P =/= q /\ X = ( P .\/ q ) ) )