Metamath Proof Explorer

Theorem 2llnma1b

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

Ref Expression
Hypotheses 2llnma1b.b ⊢ B = Base K
2llnma1b.l ⊢ ≤ ˙ = ≤ K
2llnma1b.j ⊢ ∨ ˙ = join ⁡ K
2llnma1b.m ⊢ ∧ ˙ = meet ⁡ K
2llnma1b.a ⊢ A = Atoms ⁡ K
Assertion 2llnma1b ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ P ∨ ˙ X → P ∨ ˙ X ∧ ˙ P ∨ ˙ Q = P

Proof

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