Metamath Proof Explorer

Theorem cdlemg8b

Description: TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013)

Ref Expression
Hypotheses cdlemg8.l ⊢≤˙=≤K
cdlemg8.j ⊢∨˙=join⁡K
cdlemg8.m ⊢∧˙=meet⁡K
cdlemg8.a ⊢A=Atoms⁡K
cdlemg8.h ⊢H=LHyp⁡K
cdlemg8.t ⊢T=LTrn⁡K⁡W
Assertion cdlemg8b ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∨˙F⁡G⁡P=P∨˙Q

Proof

Step Hyp Ref Expression
1 cdlemg8.l ⊢≤˙=≤K
2 cdlemg8.j ⊢∨˙=join⁡K
3 cdlemg8.m ⊢∧˙=meet⁡K
4 cdlemg8.a ⊢A=Atoms⁡K
5 cdlemg8.h ⊢H=LHyp⁡K
6 cdlemg8.t ⊢T=LTrn⁡K⁡W
7 simp1l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→K∈HL
8 7 hllatd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→K∈Lat
9 simp21l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∈A
10 eqid ⊢BaseK=BaseK
11 10 4 atbase ⊢P∈A→P∈BaseK
12 9 11 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∈BaseK
13 simp22l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→Q∈A
14 10 4 atbase ⊢Q∈A→Q∈BaseK
15 13 14 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→Q∈BaseK
16 10 1 2 latlej1 ⊢K∈Lat∧P∈BaseK∧Q∈BaseK→P≤˙P∨˙Q
17 8 12 15 16 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P≤˙P∨˙Q
18 simp1 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→K∈HL∧W∈H
19 simp23 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F∈T
20 simp31 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→G∈T
21 simp21 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∈A∧¬P≤˙W
22 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→G⁡P∈A∧¬G⁡P≤˙W
23 18 20 21 22 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→G⁡P∈A∧¬G⁡P≤˙W
24 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧F∈T∧G⁡P∈A∧¬G⁡P≤˙W→F⁡G⁡P∈A∧¬F⁡G⁡P≤˙W
25 24 simpld ⊢K∈HL∧W∈H∧F∈T∧G⁡P∈A∧¬G⁡P≤˙W→F⁡G⁡P∈A
26 18 19 23 25 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P∈A
27 10 4 atbase ⊢F⁡G⁡P∈A→F⁡G⁡P∈BaseK
28 26 27 syl ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P∈BaseK
29 10 5 6 ltrncl ⊢K∈HL∧W∈H∧G∈T∧Q∈BaseK→G⁡Q∈BaseK
30 18 20 15 29 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→G⁡Q∈BaseK
31 10 5 6 ltrncl ⊢K∈HL∧W∈H∧F∈T∧G⁡Q∈BaseK→F⁡G⁡Q∈BaseK
32 18 19 30 31 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡Q∈BaseK
33 10 1 2 latlej1 ⊢K∈Lat∧F⁡G⁡P∈BaseK∧F⁡G⁡Q∈BaseK→F⁡G⁡P≤˙F⁡G⁡P∨˙F⁡G⁡Q
34 8 28 32 33 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P≤˙F⁡G⁡P∨˙F⁡G⁡Q
35 simp32 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q
36 34 35 breqtrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P≤˙P∨˙Q
37 10 2 4 hlatjcl ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q∈BaseK
38 7 9 13 37 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∨˙Q∈BaseK
39 10 1 2 latjle12 ⊢K∈Lat∧P∈BaseK∧F⁡G⁡P∈BaseK∧P∨˙Q∈BaseK→P≤˙P∨˙Q∧F⁡G⁡P≤˙P∨˙Q↔P∨˙F⁡G⁡P≤˙P∨˙Q
40 8 12 28 38 39 syl13anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P≤˙P∨˙Q∧F⁡G⁡P≤˙P∨˙Q↔P∨˙F⁡G⁡P≤˙P∨˙Q
41 17 36 40 mpbi2and ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∨˙F⁡G⁡P≤˙P∨˙Q
42 simp33 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→F⁡G⁡P≠P
43 42 necomd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P≠F⁡G⁡P
44 1 2 4 ps-1 ⊢K∈HL∧P∈A∧F⁡G⁡P∈A∧P≠F⁡G⁡P∧P∈A∧Q∈A→P∨˙F⁡G⁡P≤˙P∨˙Q↔P∨˙F⁡G⁡P=P∨˙Q
45 7 9 26 43 9 13 44 syl132anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∨˙F⁡G⁡P≤˙P∨˙Q↔P∨˙F⁡G⁡P=P∨˙Q
46 41 45 mpbid ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡G⁡P∨˙F⁡G⁡Q=P∨˙Q∧F⁡G⁡P≠P→P∨˙F⁡G⁡P=P∨˙Q