Metamath Proof Explorer

Theorem 2llnma1b

Description: Generalization of 2llnma1 . (Contributed by NM, 26-Apr-2013)

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

Proof

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