Metamath Proof Explorer


Theorem lplnexatN

Description: Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l ˙ = K
lplnexat.j ˙ = join K
lplnexat.a A = Atoms K
lplnexat.n N = LLines K
lplnexat.p P = LPlanes K
Assertion lplnexatN K HL X P Y N Y ˙ X q A ¬ q ˙ Y X = Y ˙ q

Proof

Step Hyp Ref Expression
1 lplnexat.l ˙ = K
2 lplnexat.j ˙ = join K
3 lplnexat.a A = Atoms K
4 lplnexat.n N = LLines K
5 lplnexat.p P = LPlanes K
6 simp1 K HL X P Y N K HL
7 simp3 K HL X P Y N Y N
8 simp2 K HL X P Y N X P
9 6 7 8 3jca K HL X P Y N K HL Y N X P
10 eqid K = K
11 1 10 4 5 llncvrlpln2 K HL Y N X P Y ˙ X Y K X
12 9 11 sylan K HL X P Y N Y ˙ X Y K X
13 simpl1 K HL X P Y N Y ˙ X K HL
14 simpl3 K HL X P Y N Y ˙ X Y N
15 eqid Base K = Base K
16 15 4 llnbase Y N Y Base K
17 14 16 syl K HL X P Y N Y ˙ X Y Base K
18 simpl2 K HL X P Y N Y ˙ X X P
19 15 5 lplnbase X P X Base K
20 18 19 syl K HL X P Y N Y ˙ X X Base K
21 15 1 2 10 3 cvrval3 K HL Y Base K X Base K Y K X q A ¬ q ˙ Y Y ˙ q = X
22 13 17 20 21 syl3anc K HL X P Y N Y ˙ X Y K X q A ¬ q ˙ Y Y ˙ q = X
23 eqcom Y ˙ q = X X = Y ˙ q
24 23 anbi2i ¬ q ˙ Y Y ˙ q = X ¬ q ˙ Y X = Y ˙ q
25 24 rexbii q A ¬ q ˙ Y Y ˙ q = X q A ¬ q ˙ Y X = Y ˙ q
26 22 25 bitrdi K HL X P Y N Y ˙ X Y K X q A ¬ q ˙ Y X = Y ˙ q
27 12 26 mpbid K HL X P Y N Y ˙ X q A ¬ q ˙ Y X = Y ˙ q