Metamath Proof Explorer

Theorem 2lnat

Description: Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses 2lnat.b 
|- B = ( Base ` K )
2lnat.m 
|- ./\ = ( meet ` K )
2lnat.z 
|- .0. = ( 0. ` K )
2lnat.a 
|- A = ( Atoms ` K )
2lnat.n 
|- N = ( Lines ` K )
2lnat.f 
|- F = ( pmap ` K )
Assertion 2lnat 
|- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )

Proof

Step Hyp Ref Expression
1 2lnat.b 
 |-  B = ( Base ` K )
2 2lnat.m 
 |-  ./\ = ( meet ` K )
3 2lnat.z 
 |-  .0. = ( 0. ` K )
4 2lnat.a 
 |-  A = ( Atoms ` K )
5 2lnat.n 
 |-  N = ( Lines ` K )
6 2lnat.f 
 |-  F = ( pmap ` K )
7 simp11 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. HL )
8 hlatl 
 |-  ( K e. HL -> K e. AtLat )
9 7 8 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. AtLat )
10 7 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. Lat )
11 simp12 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> X e. B )
12 simp13 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> Y e. B )
13 1 2 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
14 10 11 12 13 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. B )
15 simp3r 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) =/= .0. )
16 eqid 
 |-  ( le ` K ) = ( le ` K )
17 1 16 3 4 atlex 
 |-  ( ( K e. AtLat /\ ( X ./\ Y ) e. B /\ ( X ./\ Y ) =/= .0. ) -> E. p e. A p ( le ` K ) ( X ./\ Y ) )
18 9 14 15 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> E. p e. A p ( le ` K ) ( X ./\ Y ) )
19 simp13l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> X =/= Y )
20 simp11 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( K e. HL /\ X e. B /\ Y e. B ) )
21 simp12l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( F ` X ) e. N )
22 simp12r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( F ` Y ) e. N )
23 1 16 5 6 lncmp 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) ) -> ( X ( le ` K ) Y <-> X = Y ) )
24 20 21 22 23 syl12anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ( le ` K ) Y <-> X = Y ) )
25 simp111 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. HL )
26 25 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. Lat )
27 simp112 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> X e. B )
28 simp113 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> Y e. B )
29 1 16 2 latleeqm1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ( le ` K ) Y <-> ( X ./\ Y ) = X ) )
30 26 27 28 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ( le ` K ) Y <-> ( X ./\ Y ) = X ) )
31 24 30 bitr3d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X = Y <-> ( X ./\ Y ) = X ) )
32 31 necon3bid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X =/= Y <-> ( X ./\ Y ) =/= X ) )
33 19 32 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) =/= X )
34 simp3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p ( le ` K ) ( X ./\ Y ) )
35 1 16 2 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) ( le ` K ) X )
36 26 27 28 35 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) ( le ` K ) X )
37 hlpos 
 |-  ( K e. HL -> K e. Poset )
38 25 37 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. Poset )
39 1 4 atbase 
 |-  ( p e. A -> p e. B )
40 39 3ad2ant2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p e. B )
41 26 27 28 13 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) e. B )
42 simp2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p e. A )
43 1 16 26 40 41 27 34 36 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p ( le ` K ) X )
44 eqid 
 |-  (
45 1 16 44 4 5 6 lncvrat 
 |-  ( ( ( K e. HL /\ X e. B /\ p e. A ) /\ ( ( F ` X ) e. N /\ p ( le ` K ) X ) ) -> p (
46 25 27 42 21 43 45 syl32anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p (
47 1 16 44 cvrnbtwn4 
 |-  ( ( K e. Poset /\ ( p e. B /\ X e. B /\ ( X ./\ Y ) e. B ) /\ p (  ( ( p ( le ` K ) ( X ./\ Y ) /\ ( X ./\ Y ) ( le ` K ) X ) <-> ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) ) )
48 38 40 27 41 46 47 syl131anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( ( p ( le ` K ) ( X ./\ Y ) /\ ( X ./\ Y ) ( le ` K ) X ) <-> ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) ) )
49 34 36 48 mpbi2and 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) )
50 neor 
 |-  ( ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) <-> ( p =/= ( X ./\ Y ) -> ( X ./\ Y ) = X ) )
51 49 50 sylib 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( p =/= ( X ./\ Y ) -> ( X ./\ Y ) = X ) )
52 51 necon1d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( ( X ./\ Y ) =/= X -> p = ( X ./\ Y ) ) )
53 33 52 mpd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p = ( X ./\ Y ) )
54 53 3exp 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( p e. A -> ( p ( le ` K ) ( X ./\ Y ) -> p = ( X ./\ Y ) ) ) )
55 54 reximdvai 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( E. p e. A p ( le ` K ) ( X ./\ Y ) -> E. p e. A p = ( X ./\ Y ) ) )
56 18 55 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> E. p e. A p = ( X ./\ Y ) )
57 risset 
 |-  ( ( X ./\ Y ) e. A <-> E. p e. A p = ( X ./\ Y ) )
58 56 57 sylibr 
 |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( ( F ` X ) e. N /\ ( F ` Y ) e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )