Metamath Proof Explorer


Theorem atlen0

Description: A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses atlen0.b B = Base K
atlen0.l ˙ = K
atlen0.z 0 ˙ = 0. K
atlen0.a A = Atoms K
Assertion atlen0 K AtLat X B P A P ˙ X X 0 ˙

Proof

Step Hyp Ref Expression
1 atlen0.b B = Base K
2 atlen0.l ˙ = K
3 atlen0.z 0 ˙ = 0. K
4 atlen0.a A = Atoms K
5 simpl1 K AtLat X B P A P ˙ X K AtLat
6 1 3 atl0cl K AtLat 0 ˙ B
7 5 6 syl K AtLat X B P A P ˙ X 0 ˙ B
8 simpl2 K AtLat X B P A P ˙ X X B
9 5 7 8 3jca K AtLat X B P A P ˙ X K AtLat 0 ˙ B X B
10 simpl3 K AtLat X B P A P ˙ X P A
11 1 4 atbase P A P B
12 10 11 syl K AtLat X B P A P ˙ X P B
13 eqid K = K
14 3 13 4 atcvr0 K AtLat P A 0 ˙ K P
15 5 10 14 syl2anc K AtLat X B P A P ˙ X 0 ˙ K P
16 eqid < K = < K
17 1 16 13 cvrlt K AtLat 0 ˙ B P B 0 ˙ K P 0 ˙ < K P
18 5 7 12 15 17 syl31anc K AtLat X B P A P ˙ X 0 ˙ < K P
19 simpr K AtLat X B P A P ˙ X P ˙ X
20 atlpos K AtLat K Poset
21 5 20 syl K AtLat X B P A P ˙ X K Poset
22 1 2 16 pltletr K Poset 0 ˙ B P B X B 0 ˙ < K P P ˙ X 0 ˙ < K X
23 21 7 12 8 22 syl13anc K AtLat X B P A P ˙ X 0 ˙ < K P P ˙ X 0 ˙ < K X
24 18 19 23 mp2and K AtLat X B P A P ˙ X 0 ˙ < K X
25 16 pltne K AtLat 0 ˙ B X B 0 ˙ < K X 0 ˙ X
26 9 24 25 sylc K AtLat X B P A P ˙ X 0 ˙ X
27 26 necomd K AtLat X B P A P ˙ X X 0 ˙