Metamath Proof Explorer

Theorem 2atjm

Description: The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses 2atjm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2atjm.l ⊢ ≤ = ( le ‘ 𝐾 )
2atjm.j ⊢ ∨ = ( join ‘ 𝐾 )
2atjm.m ⊢ ∧ = ( meet ‘ 𝐾 )
2atjm.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2atjm ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = 𝑃 )

Proof

Step Hyp Ref Expression
1 2atjm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 2atjm.l ⊢ ≤ = ( le ‘ 𝐾 )
3 2atjm.j ⊢ ∨ = ( join ‘ 𝐾 )
4 2atjm.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 2atjm.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
8 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
9 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
10 8 9 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
11 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐴 )
12 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
13 11 12 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐵 )
14 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
15 7 10 13 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
16 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≤ 𝑋 )
17 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
18 1 3 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
19 17 8 11 18 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
20 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
21 1 2 4 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≤ 𝑋 ) ↔ 𝑃 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
22 7 10 19 20 21 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑃 ≤ 𝑋 ) ↔ 𝑃 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
23 15 16 22 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) )
24 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
25 24 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝐾 ∈ AtLat )
26 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) )
27 7 19 20 26 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) )
28 20 8 11 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
29 nbrne2 ⊢ ( ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑃 ≠ 𝑄 )
30 29 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑄 )
31 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ¬ 𝑄 ≤ 𝑋 )
32 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
33 7 20 13 32 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝐵 )
34 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
35 7 20 13 34 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑄 ) )
36 1 2 7 10 20 33 16 35 lattrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) )
37 1 2 3 4 5 cvrat3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
38 37 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
39 17 28 30 31 36 38 syl23anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
40 27 39 eqeltrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )
41 2 5 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 ) → ( 𝑃 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ↔ 𝑃 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
42 25 8 40 41 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑃 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ↔ 𝑃 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ) )
43 23 42 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → 𝑃 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) )
44 43 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = 𝑃 )