Metamath Proof Explorer

Theorem cdleme0cp

Description: Part of proof of Lemma E in Crawley p. 113. TODO: Reformat as in cdlemg3a - swap consequent equality; make antecedent use df-3an . (Contributed by NM, 13-Jun-2012)

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 cdleme0cp ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ 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 ⊢ P ∨ ˙ U = P ∨ ˙ P ∨ ˙ Q ∧ ˙ W
8 simpll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → K ∈ HL
9 simprll ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∈ A
10 hllat ⊢ K ∈ HL → K ∈ Lat
11 10 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → K ∈ Lat
12 eqid ⊢ Base K = Base K
13 12 4 atbase ⊢ P ∈ A → P ∈ Base K
14 9 13 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∈ Base K
15 simprr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → Q ∈ A
16 12 4 atbase ⊢ Q ∈ A → Q ∈ Base K
17 15 16 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → Q ∈ Base K
18 12 2 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ Q ∈ Base K
19 11 14 17 18 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
20 12 5 lhpbase ⊢ W ∈ H → W ∈ Base K
21 20 ad2antlr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → W ∈ Base K
22 1 2 4 hlatlej1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≤ ˙ P ∨ ˙ Q
23 8 9 15 22 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ≤ ˙ P ∨ ˙ Q
24 12 1 2 3 4 atmod3i1 ⊢ K ∈ HL ∧ P ∈ A ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K ∧ P ≤ ˙ P ∨ ˙ Q → P ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q ∧ ˙ P ∨ ˙ W
25 8 9 19 21 23 24 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q ∧ ˙ P ∨ ˙ W
26 eqid ⊢ 1. ⁡ K = 1. ⁡ K
27 1 2 26 4 5 lhpjat2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1. ⁡ K
28 27 adantrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ W = 1. ⁡ K
29 28 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q ∧ ˙ P ∨ ˙ W = P ∨ ˙ Q ∧ ˙ 1. ⁡ K
30 hlol ⊢ K ∈ HL → K ∈ OL
31 30 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → K ∈ OL
32 12 3 26 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ Q ∈ Base K → P ∨ ˙ Q ∧ ˙ 1. ⁡ K = P ∨ ˙ Q
33 31 19 32 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ Q ∧ ˙ 1. ⁡ K = P ∨ ˙ Q
34 25 29 33 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ P ∨ ˙ Q ∧ ˙ W = P ∨ ˙ Q
35 7 34 syl5eq ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A → P ∨ ˙ U = P ∨ ˙ Q