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 𝐵 = ( Base ‘ 𝐾 )
cvlexch.l = ( le ‘ 𝐾 )
cvlexch.j = ( join ‘ 𝐾 )
cvlexch.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlexch2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑃 ( 𝑄 𝑋 ) → 𝑄 ( 𝑃 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cvlexch.b 𝐵 = ( Base ‘ 𝐾 )
2 cvlexch.l = ( le ‘ 𝐾 )
3 cvlexch.j = ( join ‘ 𝐾 )
4 cvlexch.a 𝐴 = ( Atoms ‘ 𝐾 )
5 1 2 3 4 cvlexch1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑃 ( 𝑋 𝑄 ) → 𝑄 ( 𝑋 𝑃 ) ) )
6 cvllat ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
7 6 3ad2ant1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝐾 ∈ Lat )
8 simp22 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝑄𝐴 )
9 1 4 atbase ( 𝑄𝐴𝑄𝐵 )
10 8 9 syl ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝑄𝐵 )
11 simp23 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝑋𝐵 )
12 1 3 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑄𝐵𝑋𝐵 ) → ( 𝑄 𝑋 ) = ( 𝑋 𝑄 ) )
13 7 10 11 12 syl3anc ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑄 𝑋 ) = ( 𝑋 𝑄 ) )
14 13 breq2d ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑃 ( 𝑄 𝑋 ) ↔ 𝑃 ( 𝑋 𝑄 ) ) )
15 simp21 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝑃𝐴 )
16 1 4 atbase ( 𝑃𝐴𝑃𝐵 )
17 15 16 syl ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → 𝑃𝐵 )
18 1 3 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑋𝐵 ) → ( 𝑃 𝑋 ) = ( 𝑋 𝑃 ) )
19 7 17 11 18 syl3anc ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑃 𝑋 ) = ( 𝑋 𝑃 ) )
20 19 breq2d ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑄 ( 𝑃 𝑋 ) ↔ 𝑄 ( 𝑋 𝑃 ) ) )
21 5 14 20 3imtr4d ( ( 𝐾 ∈ CvLat ∧ ( 𝑃𝐴𝑄𝐴𝑋𝐵 ) ∧ ¬ 𝑃 𝑋 ) → ( 𝑃 ( 𝑄 𝑋 ) → 𝑄 ( 𝑃 𝑋 ) ) )