Metamath Proof Explorer

Theorem cdleme8

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C represents s_1. In their notation, we prove p \/ s_1 = p \/ s. (Contributed by NM, 9-Jun-2012)

Ref Expression
Hypotheses cdleme8.l ⊢ ≤ ˙ = ≤ K
cdleme8.j ⊢ ∨ ˙ = join ⁡ K
cdleme8.m ⊢ ∧ ˙ = meet ⁡ K
cdleme8.a ⊢ A = Atoms ⁡ K
cdleme8.h ⊢ H = LHyp ⁡ K
cdleme8.4 ⊢ C = P ∨ ˙ S ∧ ˙ W
Assertion cdleme8 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ C = P ∨ ˙ S

Proof

Step Hyp Ref Expression
1 cdleme8.l ⊢ ≤ ˙ = ≤ K
2 cdleme8.j ⊢ ∨ ˙ = join ⁡ K
3 cdleme8.m ⊢ ∧ ˙ = meet ⁡ K
4 cdleme8.a ⊢ A = Atoms ⁡ K
5 cdleme8.h ⊢ H = LHyp ⁡ K
6 cdleme8.4 ⊢ C = P ∨ ˙ S ∧ ˙ W
7 6 oveq2i ⊢ P ∨ ˙ C = P ∨ ˙ P ∨ ˙ S ∧ ˙ W
8 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → K ∈ HL
9 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∈ A
10 8 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → K ∈ Lat
11 eqid ⊢ Base K = Base K
12 11 4 atbase ⊢ P ∈ A → P ∈ Base K
13 9 12 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∈ Base K
14 11 4 atbase ⊢ S ∈ A → S ∈ Base K
15 14 3ad2ant3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → S ∈ Base K
16 11 2 latjcl ⊢ K ∈ Lat ∧ P ∈ Base K ∧ S ∈ Base K → P ∨ ˙ S ∈ Base K
17 10 13 15 16 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ S ∈ Base K
18 simp1r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → W ∈ H
19 11 5 lhpbase ⊢ W ∈ H → W ∈ Base K
20 18 19 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → W ∈ Base K
21 11 1 2 latlej1 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ S ∈ Base K → P ≤ ˙ P ∨ ˙ S
22 10 13 15 21 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ≤ ˙ P ∨ ˙ S
23 11 1 2 3 4 atmod3i1 ⊢ K ∈ HL ∧ P ∈ A ∧ P ∨ ˙ S ∈ Base K ∧ W ∈ Base K ∧ P ≤ ˙ P ∨ ˙ S → P ∨ ˙ P ∨ ˙ S ∧ ˙ W = P ∨ ˙ S ∧ ˙ P ∨ ˙ W
24 8 9 17 20 22 23 syl131anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ P ∨ ˙ S ∧ ˙ W = P ∨ ˙ S ∧ ˙ P ∨ ˙ W
25 eqid ⊢ 1. ⁡ K = 1. ⁡ K
26 1 2 25 4 5 lhpjat2 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ W = 1. ⁡ K
27 26 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ W = 1. ⁡ K
28 27 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ S ∧ ˙ P ∨ ˙ W = P ∨ ˙ S ∧ ˙ 1. ⁡ K
29 hlol ⊢ K ∈ HL → K ∈ OL
30 8 29 syl ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → K ∈ OL
31 11 3 25 olm11 ⊢ K ∈ OL ∧ P ∨ ˙ S ∈ Base K → P ∨ ˙ S ∧ ˙ 1. ⁡ K = P ∨ ˙ S
32 30 17 31 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ S ∧ ˙ 1. ⁡ K = P ∨ ˙ S
33 24 28 32 3eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ P ∨ ˙ S ∧ ˙ W = P ∨ ˙ S
34 7 33 eqtrid ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A → P ∨ ˙ C = P ∨ ˙ S