Metamath Proof Explorer

Theorem cdlemg13

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

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 simp11 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→K∈HL∧W∈H
9 simp2l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F∈T
10 simp2r ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→G∈T
11 simp12 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∈A∧¬P≤˙W
12 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→G⁡P∈A∧¬G⁡P≤˙W
13 8 10 11 12 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→G⁡P∈A∧¬G⁡P≤˙W
14 1 2 3 4 5 6 7 trlval2 ⊢K∈HL∧W∈H∧F∈T∧G⁡P∈A∧¬G⁡P≤˙W→R⁡F=G⁡P∨˙F⁡G⁡P∧˙W
15 8 9 13 14 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→R⁡F=G⁡P∨˙F⁡G⁡P∧˙W
16 simp13 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→Q∈A∧¬Q≤˙W
17 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧Q∈A∧¬Q≤˙W→G⁡Q∈A∧¬G⁡Q≤˙W
18 8 10 16 17 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→G⁡Q∈A∧¬G⁡Q≤˙W
19 1 2 3 4 5 6 7 trlval2 ⊢K∈HL∧W∈H∧F∈T∧G⁡Q∈A∧¬G⁡Q≤˙W→R⁡F=G⁡Q∨˙F⁡G⁡Q∧˙W
20 8 9 18 19 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→R⁡F=G⁡Q∨˙F⁡G⁡Q∧˙W
21 15 20 eqtr3d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→G⁡P∨˙F⁡G⁡P∧˙W=G⁡Q∨˙F⁡G⁡Q∧˙W
22 1 2 3 4 5 6 7 cdlemg13a ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∨˙F⁡G⁡P=G⁡P∨˙F⁡G⁡P
23 22 oveq1d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∨˙F⁡G⁡P∧˙W=G⁡P∨˙F⁡G⁡P∧˙W
24 simp2 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F∈T∧G∈T
25 simp31 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡P≠P
26 1 4 5 6 ltrnatneq ⊢K∈HL∧W∈H∧F∈T∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F⁡P≠P→F⁡Q≠Q
27 8 9 11 16 25 26 syl131anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡Q≠Q
28 simp32 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→R⁡F=R⁡G
29 simp33 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q
30 simp11l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→K∈HL
31 simp12l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∈A
32 1 4 5 6 ltrncoat ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A→F⁡G⁡P∈A
33 8 24 31 32 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡G⁡P∈A
34 simp13l ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→Q∈A
35 1 4 5 6 ltrncoat ⊢K∈HL∧W∈H∧F∈T∧G∈T∧Q∈A→F⁡G⁡Q∈A
36 8 24 34 35 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡G⁡Q∈A
37 2 4 hlatjcom ⊢K∈HL∧F⁡G⁡P∈A∧F⁡G⁡Q∈A→F⁡G⁡P∨˙F⁡G⁡Q=F⁡G⁡Q∨˙F⁡G⁡P
38 30 33 36 37 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡G⁡P∨˙F⁡G⁡Q=F⁡G⁡Q∨˙F⁡G⁡P
39 2 4 hlatjcom ⊢K∈HL∧P∈A∧Q∈A→P∨˙Q=Q∨˙P
40 30 31 34 39 syl3anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∨˙Q=Q∨˙P
41 29 38 40 3netr3d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→F⁡G⁡Q∨˙F⁡G⁡P≠Q∨˙P
42 1 2 3 4 5 6 7 cdlemg13a ⊢K∈HL∧W∈H∧Q∈A∧¬Q≤˙W∧P∈A∧¬P≤˙W∧F∈T∧G∈T∧F⁡Q≠Q∧R⁡F=R⁡G∧F⁡G⁡Q∨˙F⁡G⁡P≠Q∨˙P→Q∨˙F⁡G⁡Q=G⁡Q∨˙F⁡G⁡Q
43 8 16 11 24 27 28 41 42 syl313anc ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→Q∨˙F⁡G⁡Q=G⁡Q∨˙F⁡G⁡Q
44 43 oveq1d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→Q∨˙F⁡G⁡Q∧˙W=G⁡Q∨˙F⁡G⁡Q∧˙W
45 21 23 44 3eqtr4d ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W∧Q∈A∧¬Q≤˙W∧F∈T∧G∈T∧F⁡P≠P∧R⁡F=R⁡G∧F⁡G⁡P∨˙F⁡G⁡Q≠P∨˙Q→P∨˙F⁡G⁡P∧˙W=Q∨˙F⁡G⁡Q∧˙W