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