Metamath Proof Explorer

Theorem cvlexchb1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011)

Ref Expression
Hypotheses cvlexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlexch.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlexchb1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 cvlexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvlexch.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvlexch.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvlexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cvllat ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
6 5 adantr ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
7 simpr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
8 simpr2 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑄 ∈ 𝐴 )
9 1 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
10 8 9 syl ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑄 ∈ 𝐵 )
11 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
12 6 7 10 11 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
13 12 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
15 simpr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) )
16 simpr1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑃 ∈ 𝐴 )
17 1 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
18 16 17 syl ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑃 ∈ 𝐵 )
19 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
20 6 7 10 19 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
21 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ) )
22 6 7 18 20 21 syl13anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ) )
23 22 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ) )
24 23 adantr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ↔ ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ) )
25 14 15 24 mpbi2and ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) )
26 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) )
27 6 7 18 26 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) )
28 27 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) )
29 28 adantr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) )
30 1 2 3 4 cvlexch1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )
31 30 imp ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) )
32 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
33 6 7 18 32 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
34 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) )
35 6 7 10 33 34 syl13anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) )
36 35 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) )
37 36 adantr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑃 ) ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) )
38 29 31 37 mpbi2and ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) )
39 1 2 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 ) → ( ( ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
40 6 33 20 39 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
41 40 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( ( ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
42 41 adantr ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( ( 𝑋 ∨ 𝑃 ) ≤ ( 𝑋 ∨ 𝑄 ) ∧ ( 𝑋 ∨ 𝑄 ) ≤ ( 𝑋 ∨ 𝑃 ) ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
43 25 38 42 mpbi2and ⊢ ( ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) )
44 43 ex ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
45 1 2 3 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → 𝑃 ≤ ( 𝑋 ∨ 𝑃 ) )
46 6 7 18 45 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑃 ≤ ( 𝑋 ∨ 𝑃 ) )
47 breq2 ⊢ ( ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑃 ) ↔ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) )
48 46 47 syl5ibcom ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) )
49 48 3adant3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) )
50 44 49 impbid ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )