Metamath Proof Explorer

Theorem cdlemi1

Description: Part of proof of Lemma I of Crawley p. 118. (Contributed by NM, 18-Jun-2013)

Ref Expression
Hypotheses cdlemi.b ⊢B=BaseK
cdlemi.l ⊢≤˙=≤K
cdlemi.j ⊢∨˙=join⁡K
cdlemi.m ⊢∧˙=meet⁡K
cdlemi.a ⊢A=Atoms⁡K
cdlemi.h ⊢H=LHyp⁡K
cdlemi.t ⊢T=LTrn⁡K⁡W
cdlemi.r ⊢R=trL⁡K⁡W
cdlemi.e ⊢E=TEndo⁡K⁡W
Assertion cdlemi1 ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G⁡P≤˙P∨˙R⁡G

Proof

Step Hyp Ref Expression
1 cdlemi.b ⊢B=BaseK
2 cdlemi.l ⊢≤˙=≤K
3 cdlemi.j ⊢∨˙=join⁡K
4 cdlemi.m ⊢∧˙=meet⁡K
5 cdlemi.a ⊢A=Atoms⁡K
6 cdlemi.h ⊢H=LHyp⁡K
7 cdlemi.t ⊢T=LTrn⁡K⁡W
8 cdlemi.r ⊢R=trL⁡K⁡W
9 cdlemi.e ⊢E=TEndo⁡K⁡W
10 simp1l ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→K∈HL
11 10 hllatd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→K∈Lat
12 simp1 ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→K∈HL∧W∈H
13 simp2l ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U∈E
14 simp2r ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→G∈T
15 6 7 9 tendocl ⊢K∈HL∧W∈H∧U∈E∧G∈T→U⁡G∈T
16 12 13 14 15 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G∈T
17 simp3l ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∈A
18 1 5 atbase ⊢P∈A→P∈B
19 17 18 syl ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∈B
20 1 6 7 ltrncl ⊢K∈HL∧W∈H∧U⁡G∈T∧P∈B→U⁡G⁡P∈B
21 12 16 19 20 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G⁡P∈B
22 1 6 7 8 trlcl ⊢K∈HL∧W∈H∧U⁡G∈T→R⁡U⁡G∈B
23 12 16 22 syl2anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→R⁡U⁡G∈B
24 1 3 latjcl ⊢K∈Lat∧P∈B∧R⁡U⁡G∈B→P∨˙R⁡U⁡G∈B
25 11 19 23 24 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙R⁡U⁡G∈B
26 1 6 7 8 trlcl ⊢K∈HL∧W∈H∧G∈T→R⁡G∈B
27 12 14 26 syl2anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→R⁡G∈B
28 1 3 latjcl ⊢K∈Lat∧P∈B∧R⁡G∈B→P∨˙R⁡G∈B
29 11 19 27 28 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙R⁡G∈B
30 1 2 3 latlej2 ⊢K∈Lat∧P∈B∧U⁡G⁡P∈B→U⁡G⁡P≤˙P∨˙U⁡G⁡P
31 11 19 21 30 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G⁡P≤˙P∨˙U⁡G⁡P
32 2 3 4 5 6 7 8 trlval2 ⊢K∈HL∧W∈H∧U⁡G∈T∧P∈A∧¬P≤˙W→R⁡U⁡G=P∨˙U⁡G⁡P∧˙W
33 16 32 syld3an2 ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→R⁡U⁡G=P∨˙U⁡G⁡P∧˙W
34 33 oveq2d ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙R⁡U⁡G=P∨˙P∨˙U⁡G⁡P∧˙W
35 1 3 latjcl ⊢K∈Lat∧P∈B∧U⁡G⁡P∈B→P∨˙U⁡G⁡P∈B
36 11 19 21 35 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙U⁡G⁡P∈B
37 simp1r ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→W∈H
38 1 6 lhpbase ⊢W∈H→W∈B
39 37 38 syl ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→W∈B
40 1 2 3 latlej1 ⊢K∈Lat∧P∈B∧U⁡G⁡P∈B→P≤˙P∨˙U⁡G⁡P
41 11 19 21 40 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P≤˙P∨˙U⁡G⁡P
42 1 2 3 4 5 atmod3i1 ⊢K∈HL∧P∈A∧P∨˙U⁡G⁡P∈B∧W∈B∧P≤˙P∨˙U⁡G⁡P→P∨˙P∨˙U⁡G⁡P∧˙W=P∨˙U⁡G⁡P∧˙P∨˙W
43 10 17 36 39 41 42 syl131anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙P∨˙U⁡G⁡P∧˙W=P∨˙U⁡G⁡P∧˙P∨˙W
44 eqid ⊢1.⁡K=1.⁡K
45 2 3 44 5 6 lhpjat2 ⊢K∈HL∧W∈H∧P∈A∧¬P≤˙W→P∨˙W=1.⁡K
46 45 3adant2 ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙W=1.⁡K
47 46 oveq2d ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙U⁡G⁡P∧˙P∨˙W=P∨˙U⁡G⁡P∧˙1.⁡K
48 hlol ⊢K∈HL→K∈OL
49 10 48 syl ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→K∈OL
50 1 4 44 olm11 ⊢K∈OL∧P∨˙U⁡G⁡P∈B→P∨˙U⁡G⁡P∧˙1.⁡K=P∨˙U⁡G⁡P
51 49 36 50 syl2anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙U⁡G⁡P∧˙1.⁡K=P∨˙U⁡G⁡P
52 47 51 eqtrd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙U⁡G⁡P∧˙P∨˙W=P∨˙U⁡G⁡P
53 34 43 52 3eqtrd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙R⁡U⁡G=P∨˙U⁡G⁡P
54 31 53 breqtrrd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G⁡P≤˙P∨˙R⁡U⁡G
55 2 6 7 8 9 tendotp ⊢K∈HL∧W∈H∧U∈E∧G∈T→R⁡U⁡G≤˙R⁡G
56 12 13 14 55 syl3anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→R⁡U⁡G≤˙R⁡G
57 1 2 3 latjlej2 ⊢K∈Lat∧R⁡U⁡G∈B∧R⁡G∈B∧P∈B→R⁡U⁡G≤˙R⁡G→P∨˙R⁡U⁡G≤˙P∨˙R⁡G
58 11 23 27 19 57 syl13anc ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→R⁡U⁡G≤˙R⁡G→P∨˙R⁡U⁡G≤˙P∨˙R⁡G
59 56 58 mpd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→P∨˙R⁡U⁡G≤˙P∨˙R⁡G
60 1 2 11 21 25 29 54 59 lattrd ⊢K∈HL∧W∈H∧U∈E∧G∈T∧P∈A∧¬P≤˙W→U⁡G⁡P≤˙P∨˙R⁡G