Metamath Proof Explorer

Theorem cdlemc1

Description: Part of proof of Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemc1.b ⊢ B = Base K
cdlemc1.l ⊢ ≤ ˙ = ≤ K
cdlemc1.j ⊢ ∨ ˙ = join ⁡ K
cdlemc1.m ⊢ ∧ ˙ = meet ⁡ K
cdlemc1.a ⊢ A = Atoms ⁡ K
cdlemc1.h ⊢ H = LHyp ⁡ K
Assertion cdlemc1 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ P ∨ ˙ X ∧ ˙ W = P ∨ ˙ X

Proof

Step Hyp Ref Expression
1 cdlemc1.b ⊢ B = Base K
2 cdlemc1.l ⊢ ≤ ˙ = ≤ K
3 cdlemc1.j ⊢ ∨ ˙ = join ⁡ K
4 cdlemc1.m ⊢ ∧ ˙ = meet ⁡ K
5 cdlemc1.a ⊢ A = Atoms ⁡ K
6 cdlemc1.h ⊢ H = LHyp ⁡ K
7 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL
8 7 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ Lat
9 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ A
10 1 5 atbase ⊢ P ∈ A → P ∈ B
11 9 10 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∈ B
12 simp2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → X ∈ B
13 1 3 latjcl ⊢ K ∈ Lat ∧ P ∈ B ∧ X ∈ B → P ∨ ˙ X ∈ B
14 8 11 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∈ B
15 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ H
16 1 6 lhpbase ⊢ W ∈ H → W ∈ B
17 15 16 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∈ B
18 1 4 latmcl ⊢ K ∈ Lat ∧ P ∨ ˙ X ∈ B ∧ W ∈ B → P ∨ ˙ X ∧ ˙ W ∈ B
19 8 14 17 18 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∧ ˙ W ∈ B
20 1 3 latjcom ⊢ K ∈ Lat ∧ P ∈ B ∧ P ∨ ˙ X ∧ ˙ W ∈ B → P ∨ ˙ P ∨ ˙ X ∧ ˙ W = P ∨ ˙ X ∧ ˙ W ∨ ˙ P
21 8 11 19 20 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ P ∨ ˙ X ∧ ˙ W = P ∨ ˙ X ∧ ˙ W ∨ ˙ P
22 1 2 3 latlej1 ⊢ K ∈ Lat ∧ P ∈ B ∧ X ∈ B → P ≤ ˙ P ∨ ˙ X
23 8 11 12 22 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ≤ ˙ P ∨ ˙ X
24 1 2 3 4 5 atmod2i1 ⊢ K ∈ HL ∧ P ∈ A ∧ P ∨ ˙ X ∈ B ∧ W ∈ B ∧ P ≤ ˙ P ∨ ˙ X → P ∨ ˙ X ∧ ˙ W ∨ ˙ P = P ∨ ˙ X ∧ ˙ W ∨ ˙ P
25 7 9 14 17 23 24 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∧ ˙ W ∨ ˙ P = P ∨ ˙ X ∧ ˙ W ∨ ˙ P
26 eqid ⊢ 1. ⁡ K = 1. ⁡ K
27 2 3 26 5 6 lhpjat1 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 1. ⁡ K
28 27 3adant2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → W ∨ ˙ P = 1. ⁡ K
29 28 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∧ ˙ W ∨ ˙ P = P ∨ ˙ X ∧ ˙ 1. ⁡ K
30 hlol ⊢ K ∈ HL → K ∈ OL
31 7 30 syl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ OL
32 1 4 26 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ X ∈ B → P ∨ ˙ X ∧ ˙ 1. ⁡ K = P ∨ ˙ X
33 31 14 32 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∧ ˙ 1. ⁡ K = P ∨ ˙ X
34 29 33 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ X ∧ ˙ W ∨ ˙ P = P ∨ ˙ X
35 21 25 34 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ P ∨ ˙ X ∧ ˙ W = P ∨ ˙ X