Metamath Proof Explorer

Theorem lnatexN

Description: There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lnatex.b 
|- B = ( Base ` K )
lnatex.l 
|- .<_ = ( le ` K )
lnatex.a 
|- A = ( Atoms ` K )
lnatex.n 
|- N = ( Lines ` K )
lnatex.m 
|- M = ( pmap ` K )
Assertion lnatexN 
|- ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> E. q e. A ( q =/= P /\ q .<_ X ) )

Proof

Step Hyp Ref Expression
1 lnatex.b 
 |-  B = ( Base ` K )
2 lnatex.l 
 |-  .<_ = ( le ` K )
3 lnatex.a 
 |-  A = ( Atoms ` K )
4 lnatex.n 
 |-  N = ( Lines ` K )
5 lnatex.m 
 |-  M = ( pmap ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 1 6 3 4 5 isline3 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. r e. A E. s e. A ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) )
8 7 biimp3a 
 |-  ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> E. r e. A E. s e. A ( r =/= s /\ X = ( r ( join ` K ) s ) ) )
9 simpl2r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> s e. A )
10 simpl3l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> r =/= s )
11 10 necomd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> s =/= r )
12 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> r = P )
13 11 12 neeqtrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> s =/= P )
14 simpl11 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> K e. HL )
15 simpl2l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> r e. A )
16 2 6 3 hlatlej2 
 |-  ( ( K e. HL /\ r e. A /\ s e. A ) -> s .<_ ( r ( join ` K ) s ) )
17 14 15 9 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> s .<_ ( r ( join ` K ) s ) )
18 simpl3r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> X = ( r ( join ` K ) s ) )
19 17 18 breqtrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> s .<_ X )
20 neeq1 
 |-  ( q = s -> ( q =/= P <-> s =/= P ) )
21 breq1 
 |-  ( q = s -> ( q .<_ X <-> s .<_ X ) )
22 20 21 anbi12d 
 |-  ( q = s -> ( ( q =/= P /\ q .<_ X ) <-> ( s =/= P /\ s .<_ X ) ) )
23 22 rspcev 
 |-  ( ( s e. A /\ ( s =/= P /\ s .<_ X ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
24 9 13 19 23 syl12anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r = P ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
25 simpl2l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> r e. A )
26 simpr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> r =/= P )
27 simpl11 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> K e. HL )
28 simpl2r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> s e. A )
29 2 6 3 hlatlej1 
 |-  ( ( K e. HL /\ r e. A /\ s e. A ) -> r .<_ ( r ( join ` K ) s ) )
30 27 25 28 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> r .<_ ( r ( join ` K ) s ) )
31 simpl3r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> X = ( r ( join ` K ) s ) )
32 30 31 breqtrrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> r .<_ X )
33 neeq1 
 |-  ( q = r -> ( q =/= P <-> r =/= P ) )
34 breq1 
 |-  ( q = r -> ( q .<_ X <-> r .<_ X ) )
35 33 34 anbi12d 
 |-  ( q = r -> ( ( q =/= P /\ q .<_ X ) <-> ( r =/= P /\ r .<_ X ) ) )
36 35 rspcev 
 |-  ( ( r e. A /\ ( r =/= P /\ r .<_ X ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
37 25 26 32 36 syl12anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) /\ r =/= P ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
38 24 37 pm2.61dane 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( r e. A /\ s e. A ) /\ ( r =/= s /\ X = ( r ( join ` K ) s ) ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
39 38 3exp 
 |-  ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> ( ( r e. A /\ s e. A ) -> ( ( r =/= s /\ X = ( r ( join ` K ) s ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) ) ) )
40 39 rexlimdvv 
 |-  ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> ( E. r e. A E. s e. A ( r =/= s /\ X = ( r ( join ` K ) s ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) ) )
41 8 40 mpd 
 |-  ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> E. q e. A ( q =/= P /\ q .<_ X ) )