Metamath Proof Explorer


Theorem llnexatN

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

Ref Expression
Hypotheses llnexat.l ˙ = K
llnexat.j ˙ = join K
llnexat.a A = Atoms K
llnexat.n N = LLines K
Assertion llnexatN K HL X N P A P ˙ X q A P q X = P ˙ q

Proof

Step Hyp Ref Expression
1 llnexat.l ˙ = K
2 llnexat.j ˙ = join K
3 llnexat.a A = Atoms K
4 llnexat.n N = LLines K
5 simp1 K HL X N P A K HL
6 simp3 K HL X N P A P A
7 simp2 K HL X N P A X N
8 5 6 7 3jca K HL X N P A K HL P A X N
9 eqid K = K
10 1 9 3 4 atcvrlln2 K HL P A X N P ˙ X P K X
11 8 10 sylan K HL X N P A P ˙ X P K X
12 simpl1 K HL X N P A P ˙ X K HL
13 simpl3 K HL X N P A P ˙ X P A
14 eqid Base K = Base K
15 14 3 atbase P A P Base K
16 13 15 syl K HL X N P A P ˙ X P Base K
17 simpl2 K HL X N P A P ˙ X X N
18 14 4 llnbase X N X Base K
19 17 18 syl K HL X N P A P ˙ X X Base K
20 14 1 2 9 3 cvrval3 K HL P Base K X Base K P K X q A ¬ q ˙ P P ˙ q = X
21 12 16 19 20 syl3anc K HL X N P A P ˙ X P K X q A ¬ q ˙ P P ˙ q = X
22 simpll1 K HL X N P A P ˙ X q A K HL
23 hlatl K HL K AtLat
24 22 23 syl K HL X N P A P ˙ X q A K AtLat
25 simpr K HL X N P A P ˙ X q A q A
26 simpll3 K HL X N P A P ˙ X q A P A
27 1 3 atncmp K AtLat q A P A ¬ q ˙ P q P
28 24 25 26 27 syl3anc K HL X N P A P ˙ X q A ¬ q ˙ P q P
29 28 anbi1d K HL X N P A P ˙ X q A ¬ q ˙ P P ˙ q = X q P P ˙ q = X
30 necom q P P q
31 eqcom P ˙ q = X X = P ˙ q
32 30 31 anbi12i q P P ˙ q = X P q X = P ˙ q
33 29 32 bitrdi K HL X N P A P ˙ X q A ¬ q ˙ P P ˙ q = X P q X = P ˙ q
34 33 rexbidva K HL X N P A P ˙ X q A ¬ q ˙ P P ˙ q = X q A P q X = P ˙ q
35 21 34 bitrd K HL X N P A P ˙ X P K X q A P q X = P ˙ q
36 11 35 mpbid K HL X N P A P ˙ X q A P q X = P ˙ q