Metamath Proof Explorer

Theorem 2llnmat

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

Ref Expression
Hypotheses 2llnmat.m 
|- ./\ = ( meet ` K )
2llnmat.z 
|- .0. = ( 0. ` K )
2llnmat.a 
|- A = ( Atoms ` K )
2llnmat.n 
|- N = ( LLines ` K )
Assertion 2llnmat 
|- ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )

Proof

Step Hyp Ref Expression
1 2llnmat.m 
 |-  ./\ = ( meet ` K )
2 2llnmat.z 
 |-  .0. = ( 0. ` K )
3 2llnmat.a 
 |-  A = ( Atoms ` K )
4 2llnmat.n 
 |-  N = ( LLines ` K )
5 simpl1 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. HL )
6 hlatl 
 |-  ( K e. HL -> K e. AtLat )
7 5 6 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. AtLat )
8 5 hllatd 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> K e. Lat )
9 simpl2 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> X e. N )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 10 4 llnbase 
 |-  ( X e. N -> X e. ( Base ` K ) )
12 9 11 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> X e. ( Base ` K ) )
13 simpl3 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> Y e. N )
14 10 4 llnbase 
 |-  ( Y e. N -> Y e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> Y e. ( Base ` K ) )
16 10 1 latmcl 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
17 8 12 15 16 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
18 simprr 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) =/= .0. )
19 eqid 
 |-  ( le ` K ) = ( le ` K )
20 10 19 2 3 atlex 
 |-  ( ( K e. AtLat /\ ( X ./\ Y ) e. ( Base ` K ) /\ ( X ./\ Y ) =/= .0. ) -> E. p e. A p ( le ` K ) ( X ./\ Y ) )
21 7 17 18 20 syl3anc 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> E. p e. A p ( le ` K ) ( X ./\ Y ) )
22 simp1rl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> X =/= Y )
23 simp1l 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( K e. HL /\ X e. N /\ Y e. N ) )
24 19 4 llncmp 
 |-  ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X ( le ` K ) Y <-> X = Y ) )
25 23 24 syl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ( le ` K ) Y <-> X = Y ) )
26 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. HL )
27 26 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. Lat )
28 simp1l2 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> X e. N )
29 28 11 syl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> X e. ( Base ` K ) )
30 simp1l3 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> Y e. N )
31 30 14 syl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> Y e. ( Base ` K ) )
32 10 19 1 latleeqm1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ( le ` K ) Y <-> ( X ./\ Y ) = X ) )
33 27 29 31 32 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ( le ` K ) Y <-> ( X ./\ Y ) = X ) )
34 25 33 bitr3d 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X = Y <-> ( X ./\ Y ) = X ) )
35 34 necon3bid 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X =/= Y <-> ( X ./\ Y ) =/= X ) )
36 22 35 mpbid 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) =/= X )
37 simp3 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p ( le ` K ) ( X ./\ Y ) )
38 10 19 1 latmle1 
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) ( le ` K ) X )
39 27 29 31 38 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) ( le ` K ) X )
40 hlpos 
 |-  ( K e. HL -> K e. Poset )
41 26 40 syl 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> K e. Poset )
42 10 3 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
43 42 3ad2ant2 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p e. ( Base ` K ) )
44 27 29 31 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( X ./\ Y ) e. ( Base ` K ) )
45 simp2 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p e. A )
46 10 19 27 43 44 29 37 39 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p ( le ` K ) X )
47 eqid 
 |-  (
48 19 47 3 4 atcvrlln2 
 |-  ( ( ( K e. HL /\ p e. A /\ X e. N ) /\ p ( le ` K ) X ) -> p (
49 26 45 28 46 48 syl31anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p (
50 10 19 47 cvrnbtwn4 
 |-  ( ( K e. Poset /\ ( p e. ( Base ` K ) /\ X e. ( Base ` K ) /\ ( X ./\ Y ) e. ( Base ` K ) ) /\ p (  ( ( p ( le ` K ) ( X ./\ Y ) /\ ( X ./\ Y ) ( le ` K ) X ) <-> ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) ) )
51 41 43 29 44 49 50 syl131anc 
 |-  ( ( ( ( K e. HL /\ X e. N /\ 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 ) ) )
52 37 39 51 mpbi2and 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) )
53 neor 
 |-  ( ( p = ( X ./\ Y ) \/ ( X ./\ Y ) = X ) <-> ( p =/= ( X ./\ Y ) -> ( X ./\ Y ) = X ) )
54 52 53 sylib 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( p =/= ( X ./\ Y ) -> ( X ./\ Y ) = X ) )
55 54 necon1d 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> ( ( X ./\ Y ) =/= X -> p = ( X ./\ Y ) ) )
56 36 55 mpd 
 |-  ( ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) /\ p e. A /\ p ( le ` K ) ( X ./\ Y ) ) -> p = ( X ./\ Y ) )
57 56 3exp 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( p e. A -> ( p ( le ` K ) ( X ./\ Y ) -> p = ( X ./\ Y ) ) ) )
58 57 reximdvai 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( E. p e. A p ( le ` K ) ( X ./\ Y ) -> E. p e. A p = ( X ./\ Y ) ) )
59 21 58 mpd 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> E. p e. A p = ( X ./\ Y ) )
60 risset 
 |-  ( ( X ./\ Y ) e. A <-> E. p e. A p = ( X ./\ Y ) )
61 59 60 sylibr 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( X =/= Y /\ ( X ./\ Y ) =/= .0. ) ) -> ( X ./\ Y ) e. A )