Metamath Proof Explorer

Theorem cdleme3e

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses cdleme1.l ⊢ ≤ ˙ = ≤ K
cdleme1.j ⊢ ∨ ˙ = join ⁡ K
cdleme1.m ⊢ ∧ ˙ = meet ⁡ K
cdleme1.a ⊢ A = Atoms ⁡ K
cdleme1.h ⊢ H = LHyp ⁡ K
cdleme1.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
cdleme1.f ⊢ F = R ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ R ∧ ˙ W
cdleme3.3 ⊢ V = P ∨ ˙ R ∧ ˙ W
Assertion cdleme3e ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → V ∈ A

Proof

Step Hyp Ref Expression
1 cdleme1.l ⊢ ≤ ˙ = ≤ K
2 cdleme1.j ⊢ ∨ ˙ = join ⁡ K
3 cdleme1.m ⊢ ∧ ˙ = meet ⁡ K
4 cdleme1.a ⊢ A = Atoms ⁡ K
5 cdleme1.h ⊢ H = LHyp ⁡ K
6 cdleme1.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
7 cdleme1.f ⊢ F = R ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ R ∧ ˙ W
8 cdleme3.3 ⊢ V = P ∨ ˙ R ∧ ˙ W
9 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → K ∈ HL ∧ W ∈ H
10 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ A ∧ ¬ P ≤ ˙ W
11 simpr3l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∈ A
12 hllat ⊢ K ∈ HL → K ∈ Lat
13 12 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → K ∈ Lat
14 eqid ⊢ Base K = Base K
15 14 4 atbase ⊢ R ∈ A → R ∈ Base K
16 11 15 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ∈ Base K
17 simpr1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ A
18 14 4 atbase ⊢ P ∈ A → P ∈ Base K
19 17 18 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∈ Base K
20 simpr2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∈ A
21 14 4 atbase ⊢ Q ∈ A → Q ∈ Base K
22 20 21 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → Q ∈ Base K
23 simpr3r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → ¬ R ≤ ˙ P ∨ ˙ Q
24 14 1 2 latnlej1l ⊢ K ∈ Lat ∧ R ∈ Base K ∧ P ∈ Base K ∧ Q ∈ Base K ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ≠ P
25 13 16 19 22 23 24 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → R ≠ P
26 25 necomd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ≠ R
27 1 2 3 4 5 lhpat ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ R ∈ A ∧ P ≠ R → P ∨ ˙ R ∧ ˙ W ∈ A
28 9 10 11 26 27 syl112anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → P ∨ ˙ R ∧ ˙ W ∈ A
29 8 28 eqeltrid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ P ∨ ˙ Q → V ∈ A