Metamath Proof Explorer


Theorem cvlatcvr1

Description: An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatcvr1.j ˙ = join K
cvlatcvr1.c C = K
cvlatcvr1.a A = Atoms K
Assertion cvlatcvr1 K OML K CLat K CvLat P A Q A P Q P C P ˙ Q

Proof

Step Hyp Ref Expression
1 cvlatcvr1.j ˙ = join K
2 cvlatcvr1.c C = K
3 cvlatcvr1.a A = Atoms K
4 simp13 K OML K CLat K CvLat P A Q A K CvLat
5 cvlatl K CvLat K AtLat
6 4 5 syl K OML K CLat K CvLat P A Q A K AtLat
7 eqid meet K = meet K
8 eqid 0. K = 0. K
9 7 8 3 atnem0 K AtLat P A Q A P Q P meet K Q = 0. K
10 6 9 syld3an1 K OML K CLat K CvLat P A Q A P Q P meet K Q = 0. K
11 eqid Base K = Base K
12 11 3 atbase P A P Base K
13 11 1 7 8 2 3 cvlcvrp K OML K CLat K CvLat P Base K Q A P meet K Q = 0. K P C P ˙ Q
14 12 13 syl3an2 K OML K CLat K CvLat P A Q A P meet K Q = 0. K P C P ˙ Q
15 10 14 bitrd K OML K CLat K CvLat P A Q A P Q P C P ˙ Q