Metamath Proof Explorer


Theorem atle

Description: Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses atle.b B = Base K
atle.l ˙ = K
atle.z 0 ˙ = 0. K
atle.a A = Atoms K
Assertion atle K HL X B X 0 ˙ p A p ˙ X

Proof

Step Hyp Ref Expression
1 atle.b B = Base K
2 atle.l ˙ = K
3 atle.z 0 ˙ = 0. K
4 atle.a A = Atoms K
5 simp1 K HL X B X 0 ˙ K HL
6 hlop K HL K OP
7 6 3ad2ant1 K HL X B X 0 ˙ K OP
8 1 3 op0cl K OP 0 ˙ B
9 7 8 syl K HL X B X 0 ˙ 0 ˙ B
10 simp2 K HL X B X 0 ˙ X B
11 simp3 K HL X B X 0 ˙ X 0 ˙
12 eqid < K = < K
13 1 12 3 opltn0 K OP X B 0 ˙ < K X X 0 ˙
14 7 10 13 syl2anc K HL X B X 0 ˙ 0 ˙ < K X X 0 ˙
15 11 14 mpbird K HL X B X 0 ˙ 0 ˙ < K X
16 eqid join K = join K
17 1 2 12 16 4 hlrelat K HL 0 ˙ B X B 0 ˙ < K X p A 0 ˙ < K 0 ˙ join K p 0 ˙ join K p ˙ X
18 5 9 10 15 17 syl31anc K HL X B X 0 ˙ p A 0 ˙ < K 0 ˙ join K p 0 ˙ join K p ˙ X
19 simpl1 K HL X B X 0 ˙ p A K HL
20 hlol K HL K OL
21 19 20 syl K HL X B X 0 ˙ p A K OL
22 1 4 atbase p A p B
23 22 adantl K HL X B X 0 ˙ p A p B
24 1 16 3 olj02 K OL p B 0 ˙ join K p = p
25 21 23 24 syl2anc K HL X B X 0 ˙ p A 0 ˙ join K p = p
26 25 breq1d K HL X B X 0 ˙ p A 0 ˙ join K p ˙ X p ˙ X
27 26 biimpd K HL X B X 0 ˙ p A 0 ˙ join K p ˙ X p ˙ X
28 27 adantld K HL X B X 0 ˙ p A 0 ˙ < K 0 ˙ join K p 0 ˙ join K p ˙ X p ˙ X
29 28 reximdva K HL X B X 0 ˙ p A 0 ˙ < K 0 ˙ join K p 0 ˙ join K p ˙ X p A p ˙ X
30 18 29 mpd K HL X B X 0 ˙ p A p ˙ X