Metamath Proof Explorer

Theorem cdleme0cq

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 25-Apr-2013)

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