Metamath Proof Explorer


Theorem llnle

Description: Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses llnle.b B = Base K
llnle.l ˙ = K
llnle.z 0 ˙ = 0. K
llnle.a A = Atoms K
llnle.n N = LLines K
Assertion llnle K HL X B X 0 ˙ ¬ X A y N y ˙ X

Proof

Step Hyp Ref Expression
1 llnle.b B = Base K
2 llnle.l ˙ = K
3 llnle.z 0 ˙ = 0. K
4 llnle.a A = Atoms K
5 llnle.n N = LLines K
6 simpll K HL X B X 0 ˙ ¬ X A K HL
7 simplr K HL X B X 0 ˙ ¬ X A X B
8 simprl K HL X B X 0 ˙ ¬ X A X 0 ˙
9 1 2 3 4 atle K HL X B X 0 ˙ p A p ˙ X
10 6 7 8 9 syl3anc K HL X B X 0 ˙ ¬ X A p A p ˙ X
11 simp1ll K HL X B X 0 ˙ ¬ X A p A p ˙ X K HL
12 1 4 atbase p A p B
13 12 3ad2ant2 K HL X B X 0 ˙ ¬ X A p A p ˙ X p B
14 simp1lr K HL X B X 0 ˙ ¬ X A p A p ˙ X X B
15 simp3 K HL X B X 0 ˙ ¬ X A p A p ˙ X p ˙ X
16 simp2 K HL X B X 0 ˙ ¬ X A p A p ˙ X p A
17 simp1rr K HL X B X 0 ˙ ¬ X A p A p ˙ X ¬ X A
18 nelne2 p A ¬ X A p X
19 16 17 18 syl2anc K HL X B X 0 ˙ ¬ X A p A p ˙ X p X
20 eqid < K = < K
21 2 20 pltval K HL p A X B p < K X p ˙ X p X
22 11 16 14 21 syl3anc K HL X B X 0 ˙ ¬ X A p A p ˙ X p < K X p ˙ X p X
23 15 19 22 mpbir2and K HL X B X 0 ˙ ¬ X A p A p ˙ X p < K X
24 eqid join K = join K
25 eqid K = K
26 1 2 20 24 25 4 hlrelat3 K HL p B X B p < K X q A p K p join K q p join K q ˙ X
27 11 13 14 23 26 syl31anc K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X
28 simp1ll K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X K HL
29 simp21 K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X p A
30 simp23 K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X q A
31 1 24 4 hlatjcl K HL p A q A p join K q B
32 28 29 30 31 syl3anc K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X p join K q B
33 simp3l K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X p K p join K q
34 1 25 4 5 llni K HL p join K q B p A p K p join K q p join K q N
35 28 32 29 33 34 syl31anc K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X p join K q N
36 simp3r K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X p join K q ˙ X
37 breq1 y = p join K q y ˙ X p join K q ˙ X
38 37 rspcev p join K q N p join K q ˙ X y N y ˙ X
39 35 36 38 syl2anc K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X y N y ˙ X
40 39 3exp K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X y N y ˙ X
41 40 3expd K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X y N y ˙ X
42 41 3imp K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X y N y ˙ X
43 42 rexlimdv K HL X B X 0 ˙ ¬ X A p A p ˙ X q A p K p join K q p join K q ˙ X y N y ˙ X
44 27 43 mpd K HL X B X 0 ˙ ¬ X A p A p ˙ X y N y ˙ X
45 44 3exp K HL X B X 0 ˙ ¬ X A p A p ˙ X y N y ˙ X
46 45 rexlimdv K HL X B X 0 ˙ ¬ X A p A p ˙ X y N y ˙ X
47 10 46 mpd K HL X B X 0 ˙ ¬ X A y N y ˙ X