Metamath Proof Explorer

Theorem cdlemg13a

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 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

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 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
9 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
10 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
11 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
12 1 4 5 6 ltrnat ⊢K∈HL∧W∈H∧G∈T∧P∈A→G⁡P∈A
13 10 11 9 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
14 1 2 4 hlatlej1 ⊢K∈HL∧P∈A∧G⁡P∈A→P≤˙P∨˙G⁡P
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→P≤˙P∨˙G⁡P
16 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
17 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
18 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
19 1 4 5 6 ltrnel ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→G⁡P∈A∧¬G⁡P≤˙W
20 10 11 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→G⁡P∈A∧¬G⁡P≤˙W
21 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
22 10 17 20 21 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
23 1 2 3 4 5 6 7 trlval2 ⊢K∈HL∧W∈H∧G∈T∧P∈A∧¬P≤˙W→R⁡G=P∨˙G⁡P∧˙W
24 10 11 18 23 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⁡G=P∨˙G⁡P∧˙W
25 16 22 24 3eqtr3d ⊢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=P∨˙G⁡P∧˙W
26 25 oveq2d ⊢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∨˙G⁡P∨˙F⁡G⁡P∧˙W=G⁡P∨˙P∨˙G⁡P∧˙W
27 1 4 5 6 ltrncoat ⊢K∈HL∧W∈H∧F∈T∧G∈T∧P∈A→F⁡G⁡P∈A
28 10 17 11 9 27 syl121anc ⊢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
29 eqid ⊢G⁡P∨˙F⁡G⁡P∧˙W=G⁡P∨˙F⁡G⁡P∧˙W
30 1 2 3 4 5 29 cdleme0cp ⊢K∈HL∧W∈H∧G⁡P∈A∧¬G⁡P≤˙W∧F⁡G⁡P∈A→G⁡P∨˙G⁡P∨˙F⁡G⁡P∧˙W=G⁡P∨˙F⁡G⁡P
31 10 20 28 30 syl12anc ⊢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∨˙G⁡P∨˙F⁡G⁡P∧˙W=G⁡P∨˙F⁡G⁡P
32 eqid ⊢P∨˙G⁡P∧˙W=P∨˙G⁡P∧˙W
33 1 2 3 4 5 32 cdleme0cq ⊢K∈HL∧W∈H∧P∈A∧G⁡P∈A∧¬G⁡P≤˙W→G⁡P∨˙P∨˙G⁡P∧˙W=P∨˙G⁡P
34 10 9 20 33 syl12anc ⊢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∨˙P∨˙G⁡P∧˙W=P∨˙G⁡P
35 26 31 34 3eqtr3rd ⊢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∨˙G⁡P=G⁡P∨˙F⁡G⁡P
36 15 35 breqtrd ⊢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≤˙G⁡P∨˙F⁡G⁡P
37 1 2 4 hlatlej2 ⊢K∈HL∧G⁡P∈A∧F⁡G⁡P∈A→F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P
38 8 13 28 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≤˙G⁡P∨˙F⁡G⁡P
39 8 hllatd ⊢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∈Lat
40 eqid ⊢BaseK=BaseK
41 40 4 atbase ⊢P∈A→P∈BaseK
42 9 41 syl ⊢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∈BaseK
43 40 4 atbase ⊢F⁡G⁡P∈A→F⁡G⁡P∈BaseK
44 28 43 syl ⊢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∈BaseK
45 40 2 4 hlatjcl ⊢K∈HL∧G⁡P∈A∧F⁡G⁡P∈A→G⁡P∨˙F⁡G⁡P∈BaseK
46 8 13 28 45 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∨˙F⁡G⁡P∈BaseK
47 40 1 2 latjle12 ⊢K∈Lat∧P∈BaseK∧F⁡G⁡P∈BaseK∧G⁡P∨˙F⁡G⁡P∈BaseK→P≤˙G⁡P∨˙F⁡G⁡P∧F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P↔P∨˙F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P
48 39 42 44 46 47 syl13anc ⊢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≤˙G⁡P∨˙F⁡G⁡P∧F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P↔P∨˙F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P
49 36 38 48 mpbi2and ⊢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
50 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
51 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
52 1 2 3 4 5 6 cdlemg11a ⊢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
53 10 18 50 17 11 51 52 syl123anc ⊢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≠P
54 53 necomd ⊢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
55 1 2 4 ps-1 ⊢K∈HL∧P∈A∧F⁡G⁡P∈A∧P≠F⁡G⁡P∧G⁡P∈A∧F⁡G⁡P∈A→P∨˙F⁡G⁡P≤˙G⁡P∨˙F⁡G⁡P↔P∨˙F⁡G⁡P=G⁡P∨˙F⁡G⁡P
56 8 9 28 54 13 28 55 syl132anc ⊢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↔P∨˙F⁡G⁡P=G⁡P∨˙F⁡G⁡P
57 49 56 mpbid ⊢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