Metamath Proof Explorer

Theorem cdlemg10a

Description: TODO: FIX COMMENT. (Contributed by NM, 3-May-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
cdlemg10.r ⊢R=trL⁡K⁡W
Assertion cdlemg10a ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∨˙F⁡G⁡P∧˙Q∨˙F⁡G⁡Q≤˙R⁡F∨˙R⁡G

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 cdlemg10.r ⊢R=trL⁡K⁡W
8 simp11 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→K∈HL∧W∈H
9 simp12 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∈A∧¬P≤˙W
10 simp13 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→Q∈A∧¬Q≤˙W
11 simp21 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→F∈T
12 simp22 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G∈T
13 simp23 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P≠Q
14 simp31 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q
15 1 2 3 4 5 6 cdlemg9 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∨˙F⁡G⁡P∧˙Q∨˙F⁡G⁡Q≤˙F⁡G⁡P∨˙G⁡P∧˙F⁡G⁡Q∨˙G⁡Q∨˙G⁡P∨˙P∧˙G⁡Q∨˙Q
16 8 9 10 11 12 13 14 15 syl133anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∨˙F⁡G⁡P∧˙Q∨˙F⁡G⁡Q≤˙F⁡G⁡P∨˙G⁡P∧˙F⁡G⁡Q∨˙G⁡Q∨˙G⁡P∨˙P∧˙G⁡Q∨˙Q
17 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→G⁡P∈A∧¬G⁡P≤˙W
18 8 12 9 17 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡P∈A∧¬G⁡P≤˙W
19 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧Q∈A∧¬Q≤˙W→G⁡Q∈A∧¬G⁡Q≤˙W
20 8 12 10 19 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡Q∈A∧¬G⁡Q≤˙W
21 simp12l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∈A
22 simp13l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→Q∈A
23 4 5 6 ltrn11at ⊢K∈HL∧W∈H∧G∈T∧P∈A∧Q∈A∧P≠Q→G⁡P≠G⁡Q
24 8 12 21 22 13 23 syl113anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡P≠G⁡Q
25 simp32 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→¬R⁡F≤˙P∨˙Q
26 1 2 3 4 5 6 7 cdlemg10c ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T→R⁡F≤˙G⁡P∨˙G⁡Q↔R⁡F≤˙P∨˙Q
27 8 9 10 11 12 26 syl122anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡F≤˙G⁡P∨˙G⁡Q↔R⁡F≤˙P∨˙Q
28 25 27 mtbird ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→¬R⁡F≤˙G⁡P∨˙G⁡Q
29 1 2 3 4 5 6 7 trlval4 ⊢K∈HL∧W∈H∧F∈T∧G⁡P∈A∧¬G⁡P≤˙W∧G⁡Q∈A∧¬G⁡Q≤˙W∧G⁡P≠G⁡Q∧¬R⁡F≤˙G⁡P∨˙G⁡Q→R⁡F=G⁡P∨˙F⁡G⁡P∧˙G⁡Q∨˙F⁡G⁡Q
30 8 11 18 20 24 28 29 syl132anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡F=G⁡P∨˙F⁡G⁡P∧˙G⁡Q∨˙F⁡G⁡Q
31 simp11l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→K∈HL
32 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧G∈T∧P∈A→G⁡P∈A
33 8 12 21 32 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡P∈A
34 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧F∈T∧G⁡P∈A→F⁡G⁡P∈A
35 8 11 33 34 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→F⁡G⁡P∈A
36 2 4 hlatjcom ⊢K∈HL∧G⁡P∈A∧F⁡G⁡P∈A→G⁡P∨˙F⁡G⁡P=F⁡G⁡P∨˙G⁡P
37 31 33 35 36 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡P∨˙F⁡G⁡P=F⁡G⁡P∨˙G⁡P
38 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧G∈T∧Q∈A→G⁡Q∈A
39 8 12 22 38 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡Q∈A
40 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧F∈T∧G⁡Q∈A→F⁡G⁡Q∈A
41 8 11 39 40 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→F⁡G⁡Q∈A
42 2 4 hlatjcom ⊢K∈HL∧G⁡Q∈A∧F⁡G⁡Q∈A→G⁡Q∨˙F⁡G⁡Q=F⁡G⁡Q∨˙G⁡Q
43 31 39 41 42 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡Q∨˙F⁡G⁡Q=F⁡G⁡Q∨˙G⁡Q
44 37 43 oveq12d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→G⁡P∨˙F⁡G⁡P∧˙G⁡Q∨˙F⁡G⁡Q=F⁡G⁡P∨˙G⁡P∧˙F⁡G⁡Q∨˙G⁡Q
45 30 44 eqtrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡F=F⁡G⁡P∨˙G⁡P∧˙F⁡G⁡Q∨˙G⁡Q
46 simp33 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→¬R⁡G≤˙P∨˙Q
47 1 2 3 4 5 6 7 trlval4 ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧P≠Q∧¬R⁡G≤˙P∨˙Q→R⁡G=P∨˙G⁡P∧˙Q∨˙G⁡Q
48 8 12 9 10 13 46 47 syl132anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡G=P∨˙G⁡P∧˙Q∨˙G⁡Q
49 2 4 hlatjcom ⊢K∈HL∧P∈A∧G⁡P∈A→P∨˙G⁡P=G⁡P∨˙P
50 31 21 33 49 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∨˙G⁡P=G⁡P∨˙P
51 2 4 hlatjcom ⊢K∈HL∧Q∈A∧G⁡Q∈A→Q∨˙G⁡Q=G⁡Q∨˙Q
52 31 22 39 51 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→Q∨˙G⁡Q=G⁡Q∨˙Q
53 50 52 oveq12d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∨˙G⁡P∧˙Q∨˙G⁡Q=G⁡P∨˙P∧˙G⁡Q∨˙Q
54 48 53 eqtrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡G=G⁡P∨˙P∧˙G⁡Q∨˙Q
55 45 54 oveq12d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→R⁡F∨˙R⁡G=F⁡G⁡P∨˙G⁡P∧˙F⁡G⁡Q∨˙G⁡Q∨˙G⁡P∨˙P∧˙G⁡Q∨˙Q
56 16 55 breqtrrd ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧P≠Q∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q∧¬R⁡F≤˙P∨˙Q∧¬R⁡G≤˙P∨˙Q→P∨˙F⁡G⁡P∧˙Q∨˙F⁡G⁡Q≤˙R⁡F∨˙R⁡G