Metamath Proof Explorer


Theorem hlrelat5N

Description: An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of Kalmbach p. 149. (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses hlrelat5.b B=BaseK
hlrelat5.l ˙=K
hlrelat5.s <˙=<K
hlrelat5.j ˙=joinK
hlrelat5.a A=AtomsK
Assertion hlrelat5N KHLXBYBX<˙YpAX<˙X˙pp˙Y

Proof

Step Hyp Ref Expression
1 hlrelat5.b B=BaseK
2 hlrelat5.l ˙=K
3 hlrelat5.s <˙=<K
4 hlrelat5.j ˙=joinK
5 hlrelat5.a A=AtomsK
6 1 2 3 5 hlrelat1 KHLXBYBX<˙YpA¬p˙Xp˙Y
7 6 imp KHLXBYBX<˙YpA¬p˙Xp˙Y
8 hllat KHLKLat
9 id XBXB
10 1 5 atbase pApB
11 ovexd pBX˙pV
12 2 3 pltval KLatXBX˙pVX<˙X˙pX˙X˙pXX˙p
13 11 12 syl3an3 KLatXBpBX<˙X˙pX˙X˙pXX˙p
14 1 2 4 latlej1 KLatXBpBX˙X˙p
15 14 biantrurd KLatXBpBXX˙pX˙X˙pXX˙p
16 13 15 bitr4d KLatXBpBX<˙X˙pXX˙p
17 1 2 4 latleeqj1 KLatpBXBp˙Xp˙X=X
18 17 3com23 KLatXBpBp˙Xp˙X=X
19 1 4 latjcom KLatXBpBX˙p=p˙X
20 19 eqeq1d KLatXBpBX˙p=Xp˙X=X
21 18 20 bitr4d KLatXBpBp˙XX˙p=X
22 21 notbid KLatXBpB¬p˙X¬X˙p=X
23 nesym XX˙p¬X˙p=X
24 22 23 bitr4di KLatXBpB¬p˙XXX˙p
25 16 24 bitr4d KLatXBpBX<˙X˙p¬p˙X
26 8 9 10 25 syl3an KHLXBpAX<˙X˙p¬p˙X
27 26 3expa KHLXBpAX<˙X˙p¬p˙X
28 27 anbi1d KHLXBpAX<˙X˙pp˙Y¬p˙Xp˙Y
29 28 rexbidva KHLXBpAX<˙X˙pp˙YpA¬p˙Xp˙Y
30 29 3adant3 KHLXBYBpAX<˙X˙pp˙YpA¬p˙Xp˙Y
31 30 adantr KHLXBYBX<˙YpAX<˙X˙pp˙YpA¬p˙Xp˙Y
32 7 31 mpbird KHLXBYBX<˙YpAX<˙X˙pp˙Y