Metamath Proof Explorer

Theorem cdleme0cq

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 25-Apr-2013)

Ref Expression
Hypotheses cdleme0.l ⊢ ≤ ˙ = ≤ K
cdleme0.j ⊢ ∨ ˙ = join ⁡ K
cdleme0.m ⊢ ∧ ˙ = meet ⁡ K
cdleme0.a ⊢ A = Atoms ⁡ K
cdleme0.h ⊢ H = LHyp ⁡ K
cdleme0.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
Assertion cdleme0cq ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ U = P ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 cdleme0.l ⊢ ≤ ˙ = ≤ K
2 cdleme0.j ⊢ ∨ ˙ = join ⁡ K
3 cdleme0.m ⊢ ∧ ˙ = meet ⁡ K
4 cdleme0.a ⊢ A = Atoms ⁡ K
5 cdleme0.h ⊢ H = LHyp ⁡ K
6 cdleme0.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
7 6 oveq2i ⊢ Q ∨ ˙ U = Q ∨ ˙ P ∨ ˙ Q ∧ ˙ W
8 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ HL
9 simprrl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ A
10 hllat ⊢ K ∈ HL → K ∈ Lat
11 10 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ Lat
12 eqid ⊢ Base K = Base K
13 12 4 atbase ⊢ P ∈ A → P ∈ Base K
14 13 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∈ Base K
15 12 4 atbase ⊢ Q ∈ A → Q ∈ Base K
16 9 15 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∈ Base K
17 12 2 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ Q ∈ Base K
18 11 14 16 17 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∨ ˙ Q ∈ Base K
19 12 5 lhpbase ⊢ W ∈ H → W ∈ Base K
20 19 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → W ∈ Base K
21 12 1 2 latlej2 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → Q ≤ ˙ P ∨ ˙ Q
22 11 14 16 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ≤ ˙ P ∨ ˙ Q
23 12 1 2 3 4 atmod3i1 ⊢ K ∈ HL ∧ Q ∈ A ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K ∧ Q ≤ ˙ P ∨ ˙ Q → Q ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q ∧ ˙ Q ∨ ˙ W
24 8 9 18 20 22 23 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q ∧ ˙ Q ∨ ˙ W
25 eqid ⊢ 1. ⁡ K = 1. ⁡ K
26 1 2 25 4 5 lhpjat2 ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ W = 1. ⁡ K
27 26 adantrl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ W = 1. ⁡ K
28 27 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∨ ˙ Q ∧ ˙ Q ∨ ˙ W = P ∨ ˙ Q ∧ ˙ 1. ⁡ K
29 hlol ⊢ K ∈ HL → K ∈ OL
30 29 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → K ∈ OL
31 12 3 25 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ Q ∈ Base K → P ∨ ˙ Q ∧ ˙ 1. ⁡ K = P ∨ ˙ Q
32 30 18 31 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → P ∨ ˙ Q ∧ ˙ 1. ⁡ K = P ∨ ˙ Q
33 24 28 32 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q
34 7 33 syl5eq ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → Q ∨ ˙ U = P ∨ ˙ Q