Metamath Proof Explorer


Theorem 2llnm2N

Description: The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnm2.l ˙ = K
2llnm2.m ˙ = meet K
2llnm2.a A = Atoms K
2llnm2.n N = LLines K
2llnm2.p P = LPlanes K
Assertion 2llnm2N K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y A

Proof

Step Hyp Ref Expression
1 2llnm2.l ˙ = K
2 2llnm2.m ˙ = meet K
3 2llnm2.a A = Atoms K
4 2llnm2.n N = LLines K
5 2llnm2.p P = LPlanes K
6 simp22 K HL X N Y N W P X ˙ W Y ˙ W X Y Y N
7 simp1 K HL X N Y N W P X ˙ W Y ˙ W X Y K HL
8 hllat K HL K Lat
9 8 3ad2ant1 K HL X N Y N W P X ˙ W Y ˙ W X Y K Lat
10 simp21 K HL X N Y N W P X ˙ W Y ˙ W X Y X N
11 eqid Base K = Base K
12 11 4 llnbase X N X Base K
13 10 12 syl K HL X N Y N W P X ˙ W Y ˙ W X Y X Base K
14 11 4 llnbase Y N Y Base K
15 6 14 syl K HL X N Y N W P X ˙ W Y ˙ W X Y Y Base K
16 11 2 latmcl K Lat X Base K Y Base K X ˙ Y Base K
17 9 13 15 16 syl3anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y Base K
18 eqid join K = join K
19 1 18 4 5 2llnjN K HL X N Y N W P X ˙ W Y ˙ W X Y X join K Y = W
20 simp23 K HL X N Y N W P X ˙ W Y ˙ W X Y W P
21 19 20 eqeltrd K HL X N Y N W P X ˙ W Y ˙ W X Y X join K Y P
22 11 1 18 latlej1 K Lat X Base K Y Base K X ˙ X join K Y
23 9 13 15 22 syl3anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ X join K Y
24 eqid K = K
25 1 24 4 5 llncvrlpln2 K HL X N X join K Y P X ˙ X join K Y X K X join K Y
26 7 10 21 23 25 syl31anc K HL X N Y N W P X ˙ W Y ˙ W X Y X K X join K Y
27 11 18 2 24 cvrexch K HL X Base K Y Base K X ˙ Y K Y X K X join K Y
28 7 13 15 27 syl3anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y K Y X K X join K Y
29 26 28 mpbird K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y K Y
30 11 24 3 4 atcvrlln K HL X ˙ Y Base K Y Base K X ˙ Y K Y X ˙ Y A Y N
31 7 17 15 29 30 syl31anc K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y A Y N
32 6 31 mpbird K HL X N Y N W P X ˙ W Y ˙ W X Y X ˙ Y A