Metamath Proof Explorer

Theorem cvrat3

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 30-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 cvrat3.b ⊢ B = Base K
2 cvrat3.l ⊢ ≤ ˙ = ≤ K
3 cvrat3.j ⊢ ∨ ˙ = join ⁡ K
4 cvrat3.m ⊢ ∧ ˙ = meet ⁡ K
5 cvrat3.a ⊢ A = Atoms ⁡ K
6 eqid ⊢ ⋖ K = ⋖ K
7 1 2 3 6 5 cvr1 ⊢ K ∈ HL ∧ X ∈ B ∧ Q ∈ A → ¬ Q ≤ ˙ X ↔ X ⋖ K X ∨ ˙ Q
8 7 3adant3r2 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → ¬ Q ≤ ˙ X ↔ X ⋖ K X ∨ ˙ Q
9 8 biimpa ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ X → X ⋖ K X ∨ ˙ Q
10 9 adantrr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ⋖ K X ∨ ˙ Q
11 hllat ⊢ K ∈ HL → K ∈ Lat
12 11 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → K ∈ Lat
13 simpr2 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ∈ A
14 1 5 atbase ⊢ P ∈ A → P ∈ B
15 13 14 syl ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ∈ B
16 simpr3 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → Q ∈ A
17 1 5 atbase ⊢ Q ∈ A → Q ∈ B
18 16 17 syl ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → Q ∈ B
19 1 3 latjcom ⊢ K ∈ Lat ∧ P ∈ B ∧ Q ∈ B → P ∨ ˙ Q = Q ∨ ˙ P
20 12 15 18 19 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q = Q ∨ ˙ P
21 20 oveq2d ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q ∨ ˙ P
22 simpr1 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∈ B
23 1 3 latjass ⊢ K ∈ Lat ∧ X ∈ B ∧ Q ∈ B ∧ P ∈ B → X ∨ ˙ Q ∨ ˙ P = X ∨ ˙ Q ∨ ˙ P
24 12 22 18 15 23 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ Q ∨ ˙ P = X ∨ ˙ Q ∨ ˙ P
25 21 24 eqtr4d ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q ∨ ˙ P
26 25 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q ∨ ˙ P
27 1 3 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Q ∈ B → X ∨ ˙ Q ∈ B
28 12 22 18 27 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ Q ∈ B
29 1 2 3 latjlej2 ⊢ K ∈ Lat ∧ P ∈ B ∧ X ∨ ˙ Q ∈ B ∧ X ∨ ˙ Q ∈ B → P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ Q ∨ ˙ P ≤ ˙ X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q
30 12 15 28 28 29 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ Q ∨ ˙ P ≤ ˙ X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q
31 30 imp ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ Q ∨ ˙ P ≤ ˙ X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q
32 26 31 eqbrtrd ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ P ∨ ˙ Q ≤ ˙ X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q
33 1 3 latjidm ⊢ K ∈ Lat ∧ X ∨ ˙ Q ∈ B → X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q = X ∨ ˙ Q
34 12 28 33 syl2anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q = X ∨ ˙ Q
35 34 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ Q ∨ ˙ X ∨ ˙ Q = X ∨ ˙ Q
36 32 35 breqtrd ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ P ∨ ˙ Q ≤ ˙ X ∨ ˙ Q
37 simpl ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → K ∈ HL
38 2 3 5 hlatlej2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → Q ≤ ˙ P ∨ ˙ Q
39 37 13 16 38 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → Q ≤ ˙ P ∨ ˙ Q
40 1 3 latjcl ⊢ K ∈ Lat ∧ P ∈ B ∧ Q ∈ B → P ∨ ˙ Q ∈ B
41 12 15 18 40 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ B
42 1 2 3 latjlej2 ⊢ K ∈ Lat ∧ Q ∈ B ∧ P ∨ ˙ Q ∈ B ∧ X ∈ B → Q ≤ ˙ P ∨ ˙ Q → X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q
43 12 18 41 22 42 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → Q ≤ ˙ P ∨ ˙ Q → X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q
44 39 43 mpd ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q
45 44 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q
46 1 3 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∨ ˙ Q ∈ B → X ∨ ˙ P ∨ ˙ Q ∈ B
47 12 22 41 46 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ P ∨ ˙ Q ∈ B
48 1 2 latasymb ⊢ K ∈ Lat ∧ X ∨ ˙ P ∨ ˙ Q ∈ B ∧ X ∨ ˙ Q ∈ B → X ∨ ˙ P ∨ ˙ Q ≤ ˙ X ∨ ˙ Q ∧ X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q ↔ X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q
49 12 47 28 48 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∨ ˙ P ∨ ˙ Q ≤ ˙ X ∨ ˙ Q ∧ X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q ↔ X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q
50 49 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ P ∨ ˙ Q ≤ ˙ X ∨ ˙ Q ∧ X ∨ ˙ Q ≤ ˙ X ∨ ˙ P ∨ ˙ Q ↔ X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q
51 36 45 50 mpbi2and ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ∨ ˙ P ∨ ˙ Q = X ∨ ˙ Q
52 51 breq2d ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≤ ˙ X ∨ ˙ Q → X ⋖ K X ∨ ˙ P ∨ ˙ Q ↔ X ⋖ K X ∨ ˙ Q
53 52 adantrl ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ⋖ K X ∨ ˙ P ∨ ˙ Q ↔ X ⋖ K X ∨ ˙ Q
54 10 53 mpbird ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ⋖ K X ∨ ˙ P ∨ ˙ Q
55 54 ex ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ⋖ K X ∨ ˙ P ∨ ˙ Q
56 1 3 4 6 cvrexch ⊢ K ∈ HL ∧ X ∈ B ∧ P ∨ ˙ Q ∈ B → X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q ↔ X ⋖ K X ∨ ˙ P ∨ ˙ Q
57 37 22 41 56 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q ↔ X ⋖ K X ∨ ˙ P ∨ ˙ Q
58 55 57 sylibrd ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q
59 58 adantr ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q
60 1 4 latmcl ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∨ ˙ Q ∈ B → X ∧ ˙ P ∨ ˙ Q ∈ B
61 12 22 41 60 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → X ∧ ˙ P ∨ ˙ Q ∈ B
62 1 3 6 5 cvrat2 ⊢ K ∈ HL ∧ X ∧ ˙ P ∨ ˙ Q ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q ∧ X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
63 62 3expia ⊢ K ∈ HL ∧ X ∧ ˙ P ∨ ˙ Q ∈ B ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ∧ X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
64 37 61 13 16 63 syl13anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ∧ X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
65 64 expdimp ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → X ∧ ˙ P ∨ ˙ Q ⋖ K P ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
66 59 65 syld ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A ∧ P ≠ Q → ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
67 66 exp4b ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ≠ Q → ¬ Q ≤ ˙ X → P ≤ ˙ X ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A
68 67 3impd ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ∧ ¬ Q ≤ ˙ X ∧ P ≤ ˙ X ∨ ˙ Q → X ∧ ˙ P ∨ ˙ Q ∈ A