Metamath Proof Explorer

Theorem 2llnm3N

Description: Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnm3.l 
|- .<_ = ( le ` K )
2llnm3.m 
|- ./\ = ( meet ` K )
2llnm3.z 
|- .0. = ( 0. ` K )
2llnm3.n 
|- N = ( LLines ` K )
2llnm3.p 
|- P = ( LPlanes ` K )
Assertion 2llnm3N 
|- ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( X ./\ Y ) =/= .0. )

Proof

Step Hyp Ref Expression
1 2llnm3.l 
 |-  .<_ = ( le ` K )
2 2llnm3.m 
 |-  ./\ = ( meet ` K )
3 2llnm3.z 
 |-  .0. = ( 0. ` K )
4 2llnm3.n 
 |-  N = ( LLines ` K )
5 2llnm3.p 
 |-  P = ( LPlanes ` K )
6 oveq1 
 |-  ( X = Y -> ( X ./\ Y ) = ( Y ./\ Y ) )
7 6 neeq1d 
 |-  ( X = Y -> ( ( X ./\ Y ) =/= .0. <-> ( Y ./\ Y ) =/= .0. ) )
8 simpl1 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> K e. HL )
9 hlatl 
 |-  ( K e. HL -> K e. AtLat )
10 8 9 syl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> K e. AtLat )
11 simpl2 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> ( X e. N /\ Y e. N /\ W e. P ) )
12 simpl3l 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> X .<_ W )
13 simpl3r 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> Y .<_ W )
14 simpr 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> X =/= Y )
15 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
16 1 2 15 4 5 2llnm2N 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X ./\ Y ) e. ( Atoms ` K ) )
17 8 11 12 13 14 16 syl113anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> ( X ./\ Y ) e. ( Atoms ` K ) )
18 3 15 atn0 
 |-  ( ( K e. AtLat /\ ( X ./\ Y ) e. ( Atoms ` K ) ) -> ( X ./\ Y ) =/= .0. )
19 10 17 18 syl2anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) /\ X =/= Y ) -> ( X ./\ Y ) =/= .0. )
20 hllat 
 |-  ( K e. HL -> K e. Lat )
21 20 3ad2ant1 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> K e. Lat )
22 simp22 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> Y e. N )
23 eqid 
 |-  ( Base ` K ) = ( Base ` K )
24 23 4 llnbase 
 |-  ( Y e. N -> Y e. ( Base ` K ) )
25 22 24 syl 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> Y e. ( Base ` K ) )
26 23 2 latmidm 
 |-  ( ( K e. Lat /\ Y e. ( Base ` K ) ) -> ( Y ./\ Y ) = Y )
27 21 25 26 syl2anc 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( Y ./\ Y ) = Y )
28 simp1 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> K e. HL )
29 3 4 llnn0 
 |-  ( ( K e. HL /\ Y e. N ) -> Y =/= .0. )
30 28 22 29 syl2anc 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> Y =/= .0. )
31 27 30 eqnetrd 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( Y ./\ Y ) =/= .0. )
32 7 19 31 pm2.61ne 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W ) ) -> ( X ./\ Y ) =/= .0. )