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 ⊢BaseK=BaseK
12 11 4 atbase ⊢P∈A→P∈BaseK
13 9 12 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧S∈A→P∈BaseK
14 11 4 atbase ⊢S∈A→S∈BaseK
15 14 3ad2ant3 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧S∈A→S∈BaseK
16 11 2 latjcl ⊢K∈Lat∧P∈BaseK∧S∈BaseK→P∨˙S∈BaseK
17 10 13 15 16 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧S∈A→P∨˙S∈BaseK
18 simp1r ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧S∈A→W∈H
19 11 5 lhpbase ⊢W∈H→W∈BaseK
20 18 19 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧S∈A→W∈BaseK
21 11 1 2 latlej1 ⊢K∈Lat∧P∈BaseK∧S∈BaseK→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∈BaseK∧W∈BaseK∧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∈BaseK→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