Metamath Proof Explorer


Theorem cvlatexchb2

Description: A version of cvlexchb2 for atoms. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatexch.l ˙ = K
cvlatexch.j ˙ = join K
cvlatexch.a A = Atoms K
Assertion cvlatexchb2 K CvLat P A Q A R A P R P ˙ Q ˙ R P ˙ R = Q ˙ R

Proof

Step Hyp Ref Expression
1 cvlatexch.l ˙ = K
2 cvlatexch.j ˙ = join K
3 cvlatexch.a A = Atoms K
4 1 2 3 cvlatexchb1 K CvLat P A Q A R A P R P ˙ R ˙ Q R ˙ P = R ˙ Q
5 cvllat K CvLat K Lat
6 5 3ad2ant1 K CvLat P A Q A R A P R K Lat
7 simp22 K CvLat P A Q A R A P R Q A
8 eqid Base K = Base K
9 8 3 atbase Q A Q Base K
10 7 9 syl K CvLat P A Q A R A P R Q Base K
11 simp23 K CvLat P A Q A R A P R R A
12 8 3 atbase R A R Base K
13 11 12 syl K CvLat P A Q A R A P R R Base K
14 8 2 latjcom K Lat Q Base K R Base K Q ˙ R = R ˙ Q
15 6 10 13 14 syl3anc K CvLat P A Q A R A P R Q ˙ R = R ˙ Q
16 15 breq2d K CvLat P A Q A R A P R P ˙ Q ˙ R P ˙ R ˙ Q
17 simp21 K CvLat P A Q A R A P R P A
18 8 3 atbase P A P Base K
19 17 18 syl K CvLat P A Q A R A P R P Base K
20 8 2 latjcom K Lat P Base K R Base K P ˙ R = R ˙ P
21 6 19 13 20 syl3anc K CvLat P A Q A R A P R P ˙ R = R ˙ P
22 21 15 eqeq12d K CvLat P A Q A R A P R P ˙ R = Q ˙ R R ˙ P = R ˙ Q
23 4 16 22 3bitr4d K CvLat P A Q A R A P R P ˙ Q ˙ R P ˙ R = Q ˙ R