Metamath Proof Explorer

Theorem cdlemg17a

Description: TODO: FIX COMMENT. (Contributed by NM, 8-May-2013)

Ref Expression
Hypotheses cdlemg12.l ⊢≤˙=≤K
cdlemg12.j ⊢∨˙=join⁡K
cdlemg12.m ⊢∧˙=meet⁡K
cdlemg12.a ⊢A=Atoms⁡K
cdlemg12.h ⊢H=LHyp⁡K
cdlemg12.t ⊢T=LTrn⁡K⁡W
cdlemg12b.r ⊢R=trL⁡K⁡W
Assertion cdlemg17a ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G⁡P≤˙P∨˙Q

Proof

Step Hyp Ref Expression
1 cdlemg12.l ⊢≤˙=≤K
2 cdlemg12.j ⊢∨˙=join⁡K
3 cdlemg12.m ⊢∧˙=meet⁡K
4 cdlemg12.a ⊢A=Atoms⁡K
5 cdlemg12.h ⊢H=LHyp⁡K
6 cdlemg12.t ⊢T=LTrn⁡K⁡W
7 cdlemg12b.r ⊢R=trL⁡K⁡W
8 eqid ⊢BaseK=BaseK
9 simp1l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→K∈HL
10 9 hllatd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→K∈Lat
11 simp1 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→K∈HL∧W∈H
12 simp3l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G∈T
13 simp2ll ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∈A
14 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧G∈T∧P∈A→G⁡P∈A
15 11 12 13 14 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G⁡P∈A
16 8 4 atbase ⊢G⁡P∈A→G⁡P∈BaseK
17 15 16 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G⁡P∈BaseK
18 8 2 4 hlatjcl ⊢K∈HL∧P∈A∧G⁡P∈A→P∨˙G⁡P∈BaseK
19 9 13 15 18 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙G⁡P∈BaseK
20 simp2rl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→Q∈A
21 8 2 4 hlatjcl ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q∈BaseK
22 9 13 20 21 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙Q∈BaseK
23 1 2 4 hlatlej2 ⊢K∈HL∧P∈A∧G⁡P∈A→G⁡P≤˙P∨˙G⁡P
24 9 13 15 23 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G⁡P≤˙P∨˙G⁡P
25 simp2l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∈A∧¬P≤˙W
26 eqid ⊢P∨˙G⁡P∧˙W=P∨˙G⁡P∧˙W
27 1 2 3 4 5 26 cdleme0cp ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧G⁡P∈A→P∨˙P∨˙G⁡P∧˙W=P∨˙G⁡P
28 11 25 15 27 syl12anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙P∨˙G⁡P∧˙W=P∨˙G⁡P
29 1 2 4 hlatlej1 ⊢K∈HL∧P∈A∧Q∈A→P≤˙P∨˙Q
30 9 13 20 29 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P≤˙P∨˙Q
31 1 2 3 4 5 6 7 trlval2 ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→R⁡G=P∨˙G⁡P∧˙W
32 11 12 25 31 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→R⁡G=P∨˙G⁡P∧˙W
33 simp3r ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→R⁡G≤˙P∨˙Q
34 32 33 eqbrtrrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙G⁡P∧˙W≤˙P∨˙Q
35 8 4 atbase ⊢P∈A→P∈BaseK
36 13 35 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∈BaseK
37 simp1r ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→W∈H
38 8 5 lhpbase ⊢W∈H→W∈BaseK
39 37 38 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→W∈BaseK
40 8 3 latmcl ⊢K∈Lat∧P∨˙G⁡P∈BaseK∧W∈BaseK→P∨˙G⁡P∧˙W∈BaseK
41 10 19 39 40 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙G⁡P∧˙W∈BaseK
42 8 1 2 latjle12 ⊢K∈Lat∧P∈BaseK∧P∨˙G⁡P∧˙W∈BaseK∧P∨˙Q∈BaseK→P≤˙P∨˙Q∧P∨˙G⁡P∧˙W≤˙P∨˙Q↔P∨˙P∨˙G⁡P∧˙W≤˙P∨˙Q
43 10 36 41 22 42 syl13anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P≤˙P∨˙Q∧P∨˙G⁡P∧˙W≤˙P∨˙Q↔P∨˙P∨˙G⁡P∧˙W≤˙P∨˙Q
44 30 34 43 mpbi2and ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙P∨˙G⁡P∧˙W≤˙P∨˙Q
45 28 44 eqbrtrrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→P∨˙G⁡P≤˙P∨˙Q
46 8 1 10 17 19 22 24 45 lattrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧G∈T∧R⁡G≤˙P∨˙Q→G⁡P≤˙P∨˙Q