Metamath Proof Explorer


Theorem cvlexch2

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012)

Ref Expression
Hypotheses cvlexch.b B = Base K
cvlexch.l ˙ = K
cvlexch.j ˙ = join K
cvlexch.a A = Atoms K
Assertion cvlexch2 K CvLat P A Q A X B ¬ P ˙ X P ˙ Q ˙ X Q ˙ P ˙ X

Proof

Step Hyp Ref Expression
1 cvlexch.b B = Base K
2 cvlexch.l ˙ = K
3 cvlexch.j ˙ = join K
4 cvlexch.a A = Atoms K
5 1 2 3 4 cvlexch1 K CvLat P A Q A X B ¬ P ˙ X P ˙ X ˙ Q Q ˙ X ˙ P
6 cvllat K CvLat K Lat
7 6 3ad2ant1 K CvLat P A Q A X B ¬ P ˙ X K Lat
8 simp22 K CvLat P A Q A X B ¬ P ˙ X Q A
9 1 4 atbase Q A Q B
10 8 9 syl K CvLat P A Q A X B ¬ P ˙ X Q B
11 simp23 K CvLat P A Q A X B ¬ P ˙ X X B
12 1 3 latjcom K Lat Q B X B Q ˙ X = X ˙ Q
13 7 10 11 12 syl3anc K CvLat P A Q A X B ¬ P ˙ X Q ˙ X = X ˙ Q
14 13 breq2d K CvLat P A Q A X B ¬ P ˙ X P ˙ Q ˙ X P ˙ X ˙ Q
15 simp21 K CvLat P A Q A X B ¬ P ˙ X P A
16 1 4 atbase P A P B
17 15 16 syl K CvLat P A Q A X B ¬ P ˙ X P B
18 1 3 latjcom K Lat P B X B P ˙ X = X ˙ P
19 7 17 11 18 syl3anc K CvLat P A Q A X B ¬ P ˙ X P ˙ X = X ˙ P
20 19 breq2d K CvLat P A Q A X B ¬ P ˙ X Q ˙ P ˙ X Q ˙ X ˙ P
21 5 14 20 3imtr4d K CvLat P A Q A X B ¬ P ˙ X P ˙ Q ˙ X Q ˙ P ˙ X