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 ˙ = K
2llnm3.m ˙ = meet K
2llnm3.z 0 ˙ = 0. K
2llnm3.n N = LLines K
2llnm3.p P = LPlanes K
Assertion 2llnm3N K HL X N Y N W P X ˙ W Y ˙ W X ˙ Y 0 ˙

Proof

Step Hyp Ref Expression
1 2llnm3.l ˙ = 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 HL X N Y N W P X ˙ W Y ˙ W X Y K HL
9 hlatl K HL K AtLat
10 8 9 syl K HL X N Y N W P X ˙ W Y ˙ W X Y K AtLat
11 simpl2 K HL X N Y N W P X ˙ W Y ˙ W X Y X N Y N W P
12 simpl3l K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ W
13 simpl3r K HL X N Y N W P X ˙ W Y ˙ W X Y Y ˙ W
14 simpr K HL X N Y N W P X ˙ W Y ˙ W X Y X Y
15 eqid Atoms K = Atoms K
16 1 2 15 4 5 2llnm2N K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y Atoms K
17 8 11 12 13 14 16 syl113anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y Atoms K
18 3 15 atn0 K AtLat X ˙ Y Atoms K X ˙ Y 0 ˙
19 10 17 18 syl2anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y 0 ˙
20 hllat K HL K Lat
21 20 3ad2ant1 K HL X N Y N W P X ˙ W Y ˙ W K Lat
22 simp22 K HL X N Y N W P X ˙ W Y ˙ W Y N
23 eqid Base K = Base K
24 23 4 llnbase Y N Y Base K
25 22 24 syl K HL X N Y N W P X ˙ W Y ˙ W Y Base K
26 23 2 latmidm K Lat Y Base K Y ˙ Y = Y
27 21 25 26 syl2anc K HL X N Y N W P X ˙ W Y ˙ W Y ˙ Y = Y
28 simp1 K HL X N Y N W P X ˙ W Y ˙ W K HL
29 3 4 llnn0 K HL Y N Y 0 ˙
30 28 22 29 syl2anc K HL X N Y N W P X ˙ W Y ˙ W Y 0 ˙
31 27 30 eqnetrd K HL X N Y N W P X ˙ W Y ˙ W Y ˙ Y 0 ˙
32 7 19 31 pm2.61ne K HL X N Y N W P X ˙ W Y ˙ W X ˙ Y 0 ˙