Metamath Proof Explorer

Theorem cvlexchb2

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

Ref Expression
Hypotheses cvlexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlexch.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlexchb2 ( ( 𝐾 ∈ 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 cvlexchb1 ⊢ ( ( 𝐾 ∈ 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 13 eqeq12d ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( ( 𝑃 ∨ 𝑋 ) = ( 𝑄 ∨ 𝑋 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
21 5 14 20 3bitr4d ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑋 ) ↔ ( 𝑃 ∨ 𝑋 ) = ( 𝑄 ∨ 𝑋 ) ) )